A1: for k being Nat
for y1, y2 being set st k in Seg F₁() & P₁[k,y1] & P₁[k,y2] holds
y1 = y2 and
A2: for k being Nat st k in Seg F₁() holds
ex x being set st P₁[k,x]

proof end;

scheme :: FINSEQ_1:sch 2
SeqLambda{ F₁() -> Nat, F₂( set ) -> set } :

ex p being FinSequence st
( len p = F₁() & ( for k being Nat st k in Seg F₁() holds
p . k = F₂(k) ) )

proof end;

theorem :: FINSEQ_1:16

for z being set
for p being FinSequence st z in p holds
ex k being Nat st
( k in dom p & z = [k,(p . k)] )

proof end;

theorem Th17: :: FINSEQ_1:17

for p, q being FinSequence st dom p = dom q & ( for k being Nat st k in dom p holds
p . k = q . k ) holds
p = q

proof end;

theorem :: FINSEQ_1:18

for p, q being FinSequence st len p = len q & ( for k being Nat st 1 <= k & k <= len p holds
p . k = q . k ) holds
p = q

proof end;

theorem Th19: :: FINSEQ_1:19

for a being natural number
for p being FinSequence holds p | (Seg a) is FinSequence

proof end;

theorem :: FINSEQ_1:20

for f being Function
for p being FinSequence st rng p c= dom f holds
f * p is FinSequence

proof end;

theorem Th21: :: FINSEQ_1:21

for a being natural number
for p, q being FinSequence st a <= len p & q = p | (Seg a) holds
( len q = a & dom q = Seg a )

proof end;

definition

let D be set ;
mode FinSequence of D -> FinSequence means :Def4: :: FINSEQ_1:def 4
rng it c= D;
existence

proof end;

end;

:: deftheorem Def4 defines FinSequence FINSEQ_1:def 4 :

Lm3: for D being set
for f being FinSequence of D holds f is PartFunc of NAT ,D

proof end;

registration

cluster {} -> FinSequence-like ;
coherence by Th14;

end;

registration

let D be set ;
cluster finite FinSequence-like M5( NAT ,D);
existence

proof end;

end;

definition

let D be set ;
:: original: FinSequence
redefine mode FinSequence of D -> FinSequence-like PartFunc of NAT ,D;
coherence by Lm3;

end;

theorem :: FINSEQ_1:22

canceled;

theorem Th23: :: FINSEQ_1:23

for a being natural number
for D being set
for p being FinSequence of D holds p | (Seg a) is FinSequence of D

proof end;

theorem :: FINSEQ_1:24

for a being natural number
for D being non empty set ex p being FinSequence of D st len p = a

proof end;

Lm4: for q being FinSequence holds
( q = {} iff len q = 0 )

proof end;

registration

cluster empty finite set ;
existence by Th14;

end;

theorem :: FINSEQ_1:25

for p being FinSequence holds
( len p = 0 iff p = {} ) by Lm4;

theorem :: FINSEQ_1:26

for p being FinSequence holds
( p = {} iff dom p = {} ) by RELAT_1:60, RELAT_1:64;

theorem :: FINSEQ_1:27

for p being FinSequence holds
( p = {} iff rng p = {} ) by RELAT_1:60, RELAT_1:64;

theorem :: FINSEQ_1:28

canceled;

theorem Th29: :: FINSEQ_1:29

for D being set holds {} is FinSequence of D

proof end;

registration

let D be set ;
cluster empty finite FinSequence-like FinSequence of D;
existence

proof end;

end;

definition

let x be set ;
func <*x*> -> set equals :: FINSEQ_1:def 5
{[1,x]};
coherence ;

end;

:: deftheorem defines <* FINSEQ_1:def 5 :

definition

let D be set ;
func <*> D -> empty FinSequence of D equals :: FINSEQ_1:def 6
{} ;
coherence by Th29;

end;

:: deftheorem defines <*> FINSEQ_1:def 6 :

theorem :: FINSEQ_1:30

canceled;

theorem :: FINSEQ_1:31

canceled;

theorem :: FINSEQ_1:32

for p being FinSequence
for D being set holds
( p = <*> D iff len p = 0 ) by Lm4;

definition

let p, q be FinSequence;
func p ^ q -> FinSequence means :Def7: :: FINSEQ_1:def 7
( dom it = Seg ((len p) + (len q)) & ( for k being Nat st k in dom p holds
it . k = p . k ) & ( for k being Nat st k in dom q holds
it . ((len p) + k) = q . k ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def7 defines ^ FINSEQ_1:def 7 :

theorem Th33: :: FINSEQ_1:33

for p, q being FinSequence holds p = (p ^ q) | (dom p)

proof end;

theorem :: FINSEQ_1:34

canceled;

theorem Th35: :: FINSEQ_1:35

for p, q being FinSequence holds len (p ^ q) = (len p) + (len q)

proof end;

theorem Th36: :: FINSEQ_1:36

for p, q being FinSequence
for k being natural number st (len p) + 1 <= k & k <= (len p) + (len q) holds
(p ^ q) . k = q . (k - (len p))

proof end;

theorem :: FINSEQ_1:37

for p, q being FinSequence
for k being natural number st len p < k & k <= len (p ^ q) holds
(p ^ q) . k = q . (k - (len p))

proof end;

theorem Th38: :: FINSEQ_1:38

for p, q being FinSequence
for k being Nat holds
( not k in dom (p ^ q) or k in dom p or ex n being Nat st
( n in dom q & k = (len p) + n ) )

proof end;

theorem Th39: :: FINSEQ_1:39

for p, q being FinSequence holds dom p c= dom (p ^ q)

proof end;

theorem Th40: :: FINSEQ_1:40

for x being set
for q, p being FinSequence st x in dom q holds
ex k being Nat st
( k = x & (len p) + k in dom (p ^ q) )

proof end;

theorem Th41: :: FINSEQ_1:41

for k being Nat
for q, p being FinSequence st k in dom q holds
(len p) + k in dom (p ^ q)

proof end;

theorem Th42: :: FINSEQ_1:42

for p, q being FinSequence holds rng p c= rng (p ^ q)

proof end;

theorem Th43: :: FINSEQ_1:43

for q, p being FinSequence holds rng q c= rng (p ^ q)

proof end;

theorem Th44: :: FINSEQ_1:44

for p, q being FinSequence holds rng (p ^ q) = (rng p) \/ (rng q)

proof end;

theorem Th45: :: FINSEQ_1:45

for p, q, r being FinSequence holds (p ^ q) ^ r = p ^ (q ^ r)

proof end;

theorem :: FINSEQ_1:46

for p, r, q being FinSequence st ( p ^ r = q ^ r or r ^ p = r ^ q ) holds
p = q

proof end;

theorem Th47: :: FINSEQ_1:47

for p being FinSequence holds
( p ^ {} = p & {} ^ p = p )

proof end;

theorem Th48: :: FINSEQ_1:48

for p, q being FinSequence st p ^ q = {} holds
( p = {} & q = {} )

proof end;

definition

let D be set ;
let p, q be FinSequence of D;
:: original: ^
redefine func p ^ q -> FinSequence of D;
coherence

proof end;

end;

Lm5: for x, y being set holds {[x,y]} is Function

proof end;

Lm6: for x, y, x1, y1 being set st [x,y] in {[x1,y1]} holds
( x = x1 & y = y1 )

proof end;

definition

let x be set ;
:: original: <*
redefine func <*x*> -> Function means :Def8: :: FINSEQ_1:def 8
( dom it = Seg 1 & it . 1 = x );
coherence by Lm5;
compatibility

proof end;

end;

:: deftheorem Def8 defines <* FINSEQ_1:def 8 :

registration

let x be set ;
cluster <*x*> -> Relation-like Function-like ;
coherence ;

end;

registration

let x be set ;
cluster <*x*> -> Relation-like Function-like finite FinSequence-like ;
coherence

proof end;

end;

theorem :: FINSEQ_1:49

canceled;

theorem Th50: :: FINSEQ_1:50

for p, q being FinSequence
for D being set st p ^ q is FinSequence of D holds
( p is FinSequence of D & q is FinSequence of D )

proof end;

definition

let x, y be set ;
func <*x,y*> -> set equals :: FINSEQ_1:def 9
<*x*> ^ <*y*>;
correctness ;
let z be set ;
func <*x,y,z*> -> set equals :: FINSEQ_1:def 10
(<*x*> ^ <*y*>) ^ <*z*>;
correctness ;

end;

:: deftheorem defines <* FINSEQ_1:def 9 :

:: deftheorem defines <* FINSEQ_1:def 10 :

registration

let x, y be set ;
cluster <*x,y*> -> Relation-like Function-like ;
coherence ;
let z be set ;
cluster <*x,y,z*> -> Relation-like Function-like ;
coherence ;

end;

registration

let x, y be set ;
cluster <*x,y*> -> Relation-like Function-like finite FinSequence-like ;
coherence ;
let z be set ;
cluster <*x,y,z*> -> Relation-like Function-like finite FinSequence-like ;
coherence ;

end;

theorem :: FINSEQ_1:51

canceled;

theorem :: FINSEQ_1:52

for x being set holds <*x*> = {[1,x]} ;

theorem :: FINSEQ_1:53

canceled;

theorem :: FINSEQ_1:54

canceled;

theorem Th55: :: FINSEQ_1:55

for x being set
for p being FinSequence holds
( p = <*x*> iff ( dom p = Seg 1 & rng p = {x} ) )

proof end;

theorem Th56: :: FINSEQ_1:56

for x being set
for p being FinSequence holds
( p = <*x*> iff ( len p = 1 & rng p = {x} ) )

proof end;

theorem Th57: :: FINSEQ_1:57

for x being set
for p being FinSequence holds
( p = <*x*> iff ( len p = 1 & p . 1 = x ) )

proof end;

theorem :: FINSEQ_1:58

for x being set
for p being FinSequence holds (<*x*> ^ p) . 1 = x

proof end;

theorem Th59: :: FINSEQ_1:59

for x being set
for p being FinSequence holds (p ^ <*x*>) . ((len p) + 1) = x

proof end;

theorem Th60: :: FINSEQ_1:60

for x, y, z being set holds
( <*x,y,z*> = <*x*> ^ <*y,z*> & <*x,y,z*> = <*x,y*> ^ <*z*> ) by Th45;

theorem Th61: :: FINSEQ_1:61

for x, y being set
for p being FinSequence holds
( p = <*x,y*> iff ( len p = 2 & p . 1 = x & p . 2 = y ) )

proof end;

theorem :: FINSEQ_1:62

for x, y, z being set
for p being FinSequence holds
( p = <*x,y,z*> iff ( len p = 3 & p . 1 = x & p . 2 = y & p . 3 = z ) )

proof end;

theorem Th63: :: FINSEQ_1:63

for p being FinSequence st p <> {} holds
ex q being FinSequence ex x being set st p = q ^ <*x*>

proof end;

definition

let D be non empty set ;
let x be Element of D;
:: original: <*
redefine func <*x*> -> FinSequence of D;
coherence

proof end;

end;

scheme :: FINSEQ_1:sch 3
IndSeq{ P₁[ FinSequence] } :

for p being FinSequence holds P₁[p]

provided

A1: P₁[ {} ] and
A2: for p being FinSequence
for x being set st P₁[p] holds
P₁[p ^ <*x*>]

proof end;

theorem :: FINSEQ_1:64

for p, q, r, s being FinSequence st p ^ q = r ^ s & len p <= len r holds
ex t being FinSequence st p ^ t = r

proof end;

definition

let D be set ;
func D * -> set means :Def11: :: FINSEQ_1:def 11
for x being set holds
( x in it iff x is FinSequence of D );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines * FINSEQ_1:def 11 :

registration

let D be set ;
cluster D * -> non empty ;
coherence

proof end;

end;

theorem :: FINSEQ_1:65

for p, q being FinSequence st rng p = rng q & p is one-to-one & q is one-to-one holds
len p = len q

proof end;

theorem :: FINSEQ_1:66

for D being set holds {} in D *

proof end;

scheme :: FINSEQ_1:sch 4
SepSeq{ F₁() -> non empty set , P₁[ FinSequence] } :

ex X being set st
for x being set holds
( x in X iff ex p being FinSequence st
( p in F₁() * & P₁[p] & x = p ) )

proof end;

definition

let IT be Function;
attr IT is FinSubsequence-like means :Def12: :: FINSEQ_1:def 12
ex k being Nat st dom IT c= Seg k;

end;

:: deftheorem Def12 defines FinSubsequence-like FINSEQ_1:def 12 :

registration

cluster FinSubsequence-like set ;
existence

proof end;

end;

definition

mode FinSubsequence is FinSubsequence-like Function;

end;

theorem :: FINSEQ_1:67

canceled;

theorem :: FINSEQ_1:68

for p being FinSequence holds p is FinSubsequence

proof end;

theorem :: FINSEQ_1:69

for X being set
for p being FinSequence holds
( p | X is FinSubsequence & X | p is FinSubsequence )

proof end;

definition

let X be set ;
given k being natural number such that A1: X c= Seg k ;
func Sgm X -> FinSequence of NAT means :Def13: :: FINSEQ_1:def 13
( rng it = X & ( for l, m, k1, k2 being natural number st 1 <= l & l < m & m <= len it & k1 = it . l & k2 = it . m holds
k1 < k2 ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines Sgm FINSEQ_1:def 13 :

theorem :: FINSEQ_1:70

canceled;

theorem Th71: :: FINSEQ_1:71

for p' being FinSubsequence holds rng (Sgm (dom p')) = dom p'

proof end;

definition

let p' be FinSubsequence;
func Seq p' -> Function equals :: FINSEQ_1:def 14
p' * (Sgm (dom p'));
coherence ;

end;

:: deftheorem defines Seq FINSEQ_1:def 14 :

registration

let p' be FinSubsequence;
cluster Seq p' -> finite FinSequence-like ;
coherence

proof end;

end;

theorem :: FINSEQ_1:72

for X being set st ex k being Nat st X c= Seg k holds
( Sgm X = {} iff X = {} )

proof end;

theorem :: FINSEQ_1:73

for D being set holds
( D is finite iff ex p being FinSequence st D = rng p )

proof end;

registration

cluster empty finite set ;
existence

proof end;

end;

registration

cluster non empty finite set ;
existence

proof end;

end;

registration

let R be finite Relation;
cluster rng R -> finite ;
coherence

proof end;

end;

theorem :: FINSEQ_1:74

for n, m being Nat st Seg n, Seg m are_equipotent holds
n = m

proof end;

theorem :: FINSEQ_1:75

for n being Nat holds Seg n,n are_equipotent by Lm1;

theorem :: FINSEQ_1:76

for n being Nat holds Card (Seg n) = Card n by Lm2;

theorem :: FINSEQ_1:77

for X being set st X is finite holds
ex n being Nat st X, Seg n are_equipotent

proof end;

theorem :: FINSEQ_1:78

( ( for n being natural number holds card (Seg n) = n ) & ( for n being Nat holds
( card n = n & card (Card n) = n ) ) )

proof end;

registration

let x be set ;
cluster <*x*> -> non empty Relation-like Function-like finite FinSequence-like ;
coherence ;

end;

registration

cluster non empty finite set ;
existence

proof end;

end;

registration

let f1 be FinSequence;
let f2 be non empty FinSequence;
cluster f1 ^ f2 -> non empty finite ;
coherence by Th48;
cluster f2 ^ f1 -> non empty finite ;
coherence by Th48;

end;

scheme :: FINSEQ_1:sch 5
SeqDEx{ F₁() -> non empty set , F₂() -> Nat, P₁[ set , set ] } :

ex p being FinSequence of F₁() st
( dom p = Seg F₂() & ( for k being Nat st k in Seg F₂() holds
P₁[k,p . k] ) )

provided

A1: for k being Nat st k in Seg F₂() holds
ex x being Element of F₁() st P₁[k,x]

proof end;

definition

let D be set ;
let p be FinSequence of D;
let m be natural number ;
func p | m -> FinSequence of D equals :: FINSEQ_1:def 15
p | (Seg m);
coherence by Th23;

end;

:: deftheorem defines | FINSEQ_1:def 15 :

registration

let D be set ;
let f be FinSequence of D;
cluster f | 0 -> empty finite FinSequence-like ;
coherence by Th4, RELAT_1:110;

end;

theorem :: FINSEQ_1:79

for D being set
for p being FinSequence of D
for m being natural number st len p <= m holds
p | m = p

proof end;

theorem :: FINSEQ_1:80

for D being set
for p being FinSequence of D
for m being natural number st m <= len p holds
len (p | m) = m

proof end;

theorem :: FINSEQ_1:81

for n being Nat
for i, m being natural number st i in Seg n holds
i + m in Seg (n + m)

proof end;

theorem :: FINSEQ_1:82

for n being Nat
for i, m being natural number st i > 0 & i + m in Seg (n + m) holds
( i in Seg n & i in Seg (n + m) )

proof end;

definition

let R be Relation;
func R [*] -> Relation means :: FINSEQ_1:def 16
for x, y being set holds
( [x,y] in it iff ( x in field R & y in field R & ex p being FinSequence st
( len p >= 1 & p . 1 = x & p . (len p) = y & ( for i being Nat st i >= 1 & i < len p holds
[(p . i),(p . (i + 1))] in R ) ) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem defines [*] FINSEQ_1:def 16 :

theorem :: FINSEQ_1:83

for D1, D2 being set st D1 c= D2 holds
D1 * c= D2 *

proof end;

registration

let D be set ;
cluster D * -> non empty functional ;
coherence

proof end;

end;

registration

let f be finite Function;
cluster dom f -> finite ;
coherence by FINSET_1:29;

end;

registration

let f be finite Function;
let x be set ;
cluster f " x -> finite ;
coherence

proof end;

end;

theorem Th8: :: FINSEQ_1:84

for p, q being FinSequence st p c= q holds
len p <= len q

proof end;

theorem Th9: :: FINSEQ_1:85

for p, q being FinSequence
for i being Nat st 1 <= i & i <= len p holds
(p ^ q) . i = p . i

proof end;

theorem Th10: :: FINSEQ_1:86

for p, q being FinSequence
for i being Nat st 1 <= i & i <= len q holds
(p ^ q) . ((len p) + i) = q . i

proof end;