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

proof end;

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

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

proof end;

theorem :: AFINSQ_1:9

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

proof end;

theorem Th10: :: AFINSQ_1:10

for p, q being XFinSequence 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 :: AFINSQ_1:11

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

proof end;

theorem Th12: :: AFINSQ_1:12

for n being Nat
for p being XFinSequence holds p | n is XFinSequence

proof end;

theorem :: AFINSQ_1:13

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

proof end;

theorem :: AFINSQ_1:14

for k being Nat
for p, q being XFinSequence st k < len p & q = p | k holds
( len q = k & dom q = k )

proof end;

registration

let D be set ;
cluster finite T-Sequence of D;
existence

proof end;

end;

definition

let D be set ;
mode XFinSequence of D is finite T-Sequence of D;

end;

theorem Th15: :: AFINSQ_1:15

for D being set
for f being XFinSequence of D holds f is PartFunc of NAT ,D

proof end;

registration

cluster {} -> T-Sequence-like ;
coherence by ORDINAL1:45;

end;

registration

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

proof end;

end;

theorem :: AFINSQ_1:16

for k being Nat
for D being set
for p being XFinSequence of D holds p | k is XFinSequence of D

proof end;

theorem :: AFINSQ_1:17

for k being Nat
for D being non empty set ex p being XFinSequence of D st len p = k

proof end;

registration

cluster empty set ;
existence by ORDINAL1:45;

end;

theorem Th18: :: AFINSQ_1:18

for p being XFinSequence holds
( len p = 0 iff p = {} )

proof end;

theorem Th19: :: AFINSQ_1:19

for D being set holds {} is XFinSequence of D

proof end;

registration

let D be set ;
cluster empty T-Sequence of D;
existence

proof end;

end;

definition

let x be set ;
func <%x%> -> set equals :: AFINSQ_1:def 2
{[0,x]};
coherence ;

end;

:: deftheorem defines <% AFINSQ_1:def 2 :

definition

let D be set ;
func <%> D -> empty XFinSequence of D equals :: AFINSQ_1:def 3
{} ;
coherence by Th19;

end;

:: deftheorem defines <%> AFINSQ_1:def 3 :

definition

let p, q be XFinSequence;
redefine func p ^ q means :Def4: :: AFINSQ_1:def 4
( dom it = (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 ) );
compatibility

proof end;

end;

:: deftheorem Def4 defines ^ AFINSQ_1:def 4 :

registration

let p, q be XFinSequence;
cluster p ^ q -> finite ;
coherence

proof end;

end;

theorem Th20: :: AFINSQ_1:20

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

proof end;

theorem Th21: :: AFINSQ_1:21

for k being Nat
for p, q being XFinSequence st len p <= k & k < (len p) + (len q) holds
(p ^ q) . k = q . (k - (len p))

proof end;

theorem :: AFINSQ_1:22

for k being Nat
for p, q being XFinSequence st len p <= k & k < len (p ^ q) holds
(p ^ q) . k = q . (k - (len p))

proof end;

theorem Th23: :: AFINSQ_1:23

for k being Nat
for p, q being XFinSequence 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 Th24: :: AFINSQ_1:24

for p, q being T-Sequence holds dom p c= dom (p ^ q)

proof end;

theorem Th25: :: AFINSQ_1:25

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

proof end;

theorem Th26: :: AFINSQ_1:26

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

proof end;

theorem Th27: :: AFINSQ_1:27

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

proof end;

theorem Th28: :: AFINSQ_1:28

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

proof end;

theorem Th29: :: AFINSQ_1:29

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

proof end;

theorem Th30: :: AFINSQ_1:30

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

proof end;

theorem :: AFINSQ_1:31

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

proof end;

theorem Th32: :: AFINSQ_1:32

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

proof end;

theorem :: AFINSQ_1:33

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

proof end;

definition

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

proof end;

end;

Lm1: 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 :Def5: :: AFINSQ_1:def 5
( dom it = 1 & it . 0 = x );
coherence by GRFUNC_1:15;
compatibility

proof end;

end;

:: deftheorem Def5 defines <% AFINSQ_1:def 5 :

registration

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

end;

registration

let x be set ;
cluster <%x%> -> Relation-like Function-like T-Sequence-like finite ;
coherence

proof end;

end;

theorem :: AFINSQ_1:34

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

proof end;

definition

let x, y be set ;
func <%x,y%> -> set equals :: AFINSQ_1:def 6
<%x%> ^ <%y%>;
correctness ;
let z be set ;
func <%x,y,z%> -> set equals :: AFINSQ_1:def 7
(<%x%> ^ <%y%>) ^ <%z%>;
correctness ;

end;

:: deftheorem defines <% AFINSQ_1:def 6 :

:: deftheorem defines <% AFINSQ_1:def 7 :

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 T-Sequence-like finite ;
coherence ;
let z be set ;
cluster <%x,y,z%> -> Relation-like Function-like T-Sequence-like finite ;
coherence ;

end;

theorem :: AFINSQ_1:35

for x being set holds <%x%> = {[0,x]} ;

theorem Th36: :: AFINSQ_1:36

for x being set
for p being XFinSequence holds
( p = <%x%> iff ( dom p = 1 & rng p = {x} ) )

proof end;

theorem Th37: :: AFINSQ_1:37

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

proof end;

theorem :: AFINSQ_1:38

for x being set
for p being XFinSequence holds
( p = <%x%> iff ( len p = 1 & p . 0 = x ) )

proof end;

theorem :: AFINSQ_1:39

for x being set
for p being XFinSequence holds (<%x%> ^ p) . 0 = x

proof end;

theorem :: AFINSQ_1:40

for x being set
for p being XFinSequence holds (p ^ <%x%>) . (len p) = x

proof end;

theorem Th41: :: AFINSQ_1:41

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

theorem Th42: :: AFINSQ_1:42

for x, y being set
for p being XFinSequence holds
( p = <%x,y%> iff ( len p = 2 & p . 0 = x & p . 1 = y ) )

proof end;

theorem :: AFINSQ_1:43

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

proof end;

theorem Th44: :: AFINSQ_1:44

for p being XFinSequence st p <> {} holds
ex q being XFinSequence 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%> -> XFinSequence of D;
coherence

proof end;

end;

scheme :: AFINSQ_1:sch 3
IndXSeq{ P₁[ XFinSequence] } :

for p being XFinSequence holds P₁[p]

provided

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

proof end;

theorem :: AFINSQ_1:45

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

proof end;

definition

let D be set ;
func D ^omega -> set means :Def8: :: AFINSQ_1:def 8
for x being set holds
( x in it iff x is XFinSequence of D );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines ^omega AFINSQ_1:def 8 :

registration

let D be set ;
cluster D ^omega -> non empty ;
coherence

proof end;

end;

theorem :: AFINSQ_1:46

for x, D being set holds
( x in D ^omega iff x is XFinSequence of D ) by Def8;

theorem :: AFINSQ_1:47

for D being set holds {} in D ^omega

proof end;

scheme :: AFINSQ_1:sch 4
SepXSeq{ F₁() -> non empty set , P₁[ XFinSequence] } :

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

proof end;

notation

let p be XFinSequence;
let i, x be set ;
synonym Replace p,i,x for p +* i,x;

end;

registration

let p be XFinSequence;
let i, x be set ;
cluster Replace p,i,x -> T-Sequence-like finite ;
coherence

proof end;

end;

theorem :: AFINSQ_1:48

for p being XFinSequence
for i being Nat
for x being set holds
( len (Replace p,i,x) = len p & ( i < len p implies (Replace p,i,x) . i = x ) & ( for j being Nat st j <> i holds
(Replace p,i,x) . j = p . j ) )

proof end;

definition

let D be non empty set ;
let p be XFinSequence of D;
let i be Nat;
let a be Element of D;
:: original: Replace
redefine func Replace p,i,a -> XFinSequence of D;
coherence

proof end;

end;