E7: for b₁ being Nat
for b₂, b₃ being set st b₁ in F₁() & P₁[b₁,b₂] & P₁[b₁,b₃] holds
b₂ = b₃ and
E8: for b₁ being Nat st b₁ in F₁() holds
ex b₂ being set st P₁[b₁,b₂]

proof end;

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

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

proof end;

theorem Th9: :: AFINSQ_1:9

for b₁ being set
for b₂ being XFinSequence st b₁ in b₂ holds
ex b₃ being Nat st
( b₃ in dom b₂ & b₁ = [b₃,(b₂ . b₃)] )

proof end;

theorem Th10: :: AFINSQ_1:10

for b₁, b₂ being XFinSequence st dom b₁ = dom b₂ & ( for b₃ being Nat st b₃ in dom b₁ holds
b₁ . b₃ = b₂ . b₃ ) holds
b₁ = b₂

proof end;

theorem Th11: :: AFINSQ_1:11

for b₁, b₂ being XFinSequence st len b₁ = len b₂ & ( for b₃ being Nat st b₃ < len b₁ holds
b₁ . b₃ = b₂ . b₃ ) holds
b₁ = b₂

proof end;

theorem Th12: :: AFINSQ_1:12

for b₁ being Nat
for b₂ being XFinSequence holds b₂ | b₁ is XFinSequence

proof end;

theorem Th13: :: AFINSQ_1:13

for b₁ being Function
for b₂ being XFinSequence st rng b₂ c= dom b₁ holds
b₁ * b₂ is XFinSequence

proof end;

theorem Th14: :: AFINSQ_1:14

for b₁ being Nat
for b₂, b₃ being XFinSequence st b₁ < len b₂ & b₃ = b₂ | b₁ holds
( len b₃ = b₁ & dom b₃ = b₁ )

proof end;

registration

let c₁ be set ;
cluster finite T-Sequence of a₁;
existence

proof end;

end;

definition

let c₁ be set ;
mode XFinSequence of a₁ is finite T-Sequence of a₁;

end;

theorem Th15: :: AFINSQ_1:15

for b₁ being set
for b₂ being XFinSequence of b₁ holds b₂ is PartFunc of NAT ,b₁

proof end;

registration

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

end;

registration

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

proof end;

end;

theorem Th16: :: AFINSQ_1:16

for b₁ being Nat
for b₂ being set
for b₃ being XFinSequence of b₂ holds b₃ | b₁ is XFinSequence of b₂

proof end;

theorem Th17: :: AFINSQ_1:17

for b₁ being Nat
for b₂ being non empty set ex b₃ being XFinSequence of b₂ st len b₃ = b₁

proof end;

registration

cluster empty set ;
existence by ORDINAL1:45;

end;

theorem Th18: :: AFINSQ_1:18

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

proof end;

theorem Th19: :: AFINSQ_1:19

for b₁ being set holds {} is XFinSequence of b₁

proof end;

registration

let c₁ be set ;
cluster empty T-Sequence of a₁;
existence

proof end;

end;

definition

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

end;

:: deftheorem Def2 defines <% AFINSQ_1:def 2 :

definition

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

end;

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

definition

let c₁, c₂ be XFinSequence;
redefine func c₁ ^ c₂ -> set means :Def4: :: AFINSQ_1:def 4
( dom a₃ = (len a₁) + (len a₂) & ( for b₁ being Nat st b₁ in dom a₁ holds
a₃ . b₁ = a₁ . b₁ ) & ( for b₁ being Nat st b₁ in dom a₂ holds
a₃ . ((len a₁) + b₁) = a₂ . b₁ ) );
compatibility

proof end;

end;

:: deftheorem Def4 defines ^ AFINSQ_1:def 4 :

registration

let c₁, c₂ be XFinSequence;
cluster a₁ ^ a₂ -> finite ;
coherence

proof end;

end;

theorem Th20: :: AFINSQ_1:20

for b₁, b₂ being XFinSequence holds len (b₁ ^ b₂) = (len b₁) + (len b₂)

proof end;

theorem Th21: :: AFINSQ_1:21

for b₁ being Nat
for b₂, b₃ being XFinSequence st len b₂ <= b₁ & b₁ < (len b₂) + (len b₃) holds
(b₂ ^ b₃) . b₁ = b₃ . (b₁ - (len b₂))

proof end;

theorem Th22: :: AFINSQ_1:22

for b₁ being Nat
for b₂, b₃ being XFinSequence st len b₂ <= b₁ & b₁ < len (b₂ ^ b₃) holds
(b₂ ^ b₃) . b₁ = b₃ . (b₁ - (len b₂))

proof end;

theorem Th23: :: AFINSQ_1:23

for b₁ being Nat
for b₂, b₃ being XFinSequence holds
( not b₁ in dom (b₂ ^ b₃) or b₁ in dom b₂ or ex b₄ being Nat st
( b₄ in dom b₃ & b₁ = (len b₂) + b₄ ) )

proof end;

theorem Th24: :: AFINSQ_1:24

for b₁, b₂ being T-Sequence holds dom b₁ c= dom (b₁ ^ b₂)

proof end;

theorem Th25: :: AFINSQ_1:25

for b₁ being set
for b₂, b₃ being XFinSequence st b₁ in dom b₂ holds
ex b₄ being Nat st
( b₄ = b₁ & (len b₃) + b₄ in dom (b₃ ^ b₂) )

proof end;

theorem Th26: :: AFINSQ_1:26

for b₁ being Nat
for b₂, b₃ being XFinSequence st b₁ in dom b₂ holds
(len b₃) + b₁ in dom (b₃ ^ b₂)

proof end;

theorem Th27: :: AFINSQ_1:27

for b₁, b₂ being XFinSequence holds rng b₁ c= rng (b₁ ^ b₂)

proof end;

theorem Th28: :: AFINSQ_1:28

for b₁, b₂ being XFinSequence holds rng b₁ c= rng (b₂ ^ b₁)

proof end;

theorem Th29: :: AFINSQ_1:29

for b₁, b₂ being XFinSequence holds rng (b₁ ^ b₂) = (rng b₁) \/ (rng b₂)

proof end;

theorem Th30: :: AFINSQ_1:30

for b₁, b₂, b₃ being XFinSequence holds (b₁ ^ b₂) ^ b₃ = b₁ ^ (b₂ ^ b₃)

proof end;

theorem Th31: :: AFINSQ_1:31

for b₁, b₂, b₃ being XFinSequence st ( b₁ ^ b₂ = b₃ ^ b₂ or b₂ ^ b₁ = b₂ ^ b₃ ) holds
b₁ = b₃

proof end;

theorem Th32: :: AFINSQ_1:32

for b₁ being XFinSequence holds
( b₁ ^ {} = b₁ & {} ^ b₁ = b₁ )

proof end;

theorem Th33: :: AFINSQ_1:33

for b₁, b₂ being XFinSequence st b₁ ^ b₂ = {} holds
( b₁ = {} & b₂ = {} )

proof end;

definition

let c₁ be set ;
let c₂, c₃ be XFinSequence of c₁;
redefine func ^ as c₂ ^ c₃ -> T-Sequence of a₁;
coherence

proof end;

end;

Lemma24: for b₁, b₂, b₃, b₄ being set st [b₁,b₂] in {[b₃,b₄]} holds
( b₁ = b₃ & b₂ = b₄ )

proof end;

definition

let c₁ be set ;
redefine func <% as <%c₁%> -> Function means :Def5: :: AFINSQ_1:def 5
( dom a₂ = 1 & a₂ . 0 = a₁ );
coherence by GRFUNC_1:15;
compatibility

proof end;

end;

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

registration

let c₁ be set ;
cluster <%a₁%> -> Relation-like Function-like ;
coherence ;

end;

registration

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

proof end;

end;

theorem Th34: :: AFINSQ_1:34

for b₁, b₂ being XFinSequence
for b₃ being set st b₁ ^ b₂ is XFinSequence of b₃ holds
( b₁ is XFinSequence of b₃ & b₂ is XFinSequence of b₃ )

proof end;

definition

let c₁, c₂ be set ;
func <%c₁,c₂%> -> set equals :: AFINSQ_1:def 6
<%a₁%> ^ <%a₂%>;
correctness ;
let c₃ be set ;
func <%c₁,c₂,c₃%> -> set equals :: AFINSQ_1:def 7
(<%a₁%> ^ <%a₂%>) ^ <%a₃%>;
correctness ;

end;

:: deftheorem Def6 defines <% AFINSQ_1:def 6 :

:: deftheorem Def7 defines <% AFINSQ_1:def 7 :

registration

let c₁, c₂ be set ;
cluster <%a₁,a₂%> -> Relation-like Function-like ;
coherence ;
let c₃ be set ;
cluster <%a₁,a₂,a₃%> -> Relation-like Function-like ;
coherence ;

end;

registration

let c₁, c₂ be set ;
cluster <%a₁,a₂%> -> Relation-like Function-like T-Sequence-like finite ;
coherence ;
let c₃ be set ;
cluster <%a₁,a₂,a₃%> -> Relation-like Function-like T-Sequence-like finite ;
coherence ;

end;

theorem Th35: :: AFINSQ_1:35

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

theorem Th36: :: AFINSQ_1:36

for b₁ being set
for b₂ being XFinSequence holds
( b₂ = <%b₁%> iff ( dom b₂ = 1 & rng b₂ = {b₁} ) )

proof end;

theorem Th37: :: AFINSQ_1:37

for b₁ being set
for b₂ being XFinSequence holds
( b₂ = <%b₁%> iff ( len b₂ = 1 & rng b₂ = {b₁} ) )

proof end;

theorem Th38: :: AFINSQ_1:38

for b₁ being set
for b₂ being XFinSequence holds
( b₂ = <%b₁%> iff ( len b₂ = 1 & b₂ . 0 = b₁ ) )

proof end;

theorem Th39: :: AFINSQ_1:39

for b₁ being set
for b₂ being XFinSequence holds (<%b₁%> ^ b₂) . 0 = b₁

proof end;

theorem Th40: :: AFINSQ_1:40

for b₁ being set
for b₂ being XFinSequence holds (b₂ ^ <%b₁%>) . (len b₂) = b₁

proof end;

theorem Th41: :: AFINSQ_1:41

for b₁, b₂, b₃ being set holds
( <%b₁,b₂,b₃%> = <%b₁%> ^ <%b₂,b₃%> & <%b₁,b₂,b₃%> = <%b₁,b₂%> ^ <%b₃%> ) by Th30;

theorem Th42: :: AFINSQ_1:42

for b₁, b₂ being set
for b₃ being XFinSequence holds
( b₃ = <%b₁,b₂%> iff ( len b₃ = 2 & b₃ . 0 = b₁ & b₃ . 1 = b₂ ) )

proof end;

theorem Th43: :: AFINSQ_1:43

for b₁, b₂, b₃ being set
for b₄ being XFinSequence holds
( b₄ = <%b₁,b₂,b₃%> iff ( len b₄ = 3 & b₄ . 0 = b₁ & b₄ . 1 = b₂ & b₄ . 2 = b₃ ) )

proof end;

theorem Th44: :: AFINSQ_1:44

for b₁ being XFinSequence st b₁ <> {} holds
ex b₂ being XFinSequenceex b₃ being set st b₁ = b₂ ^ <%b₃%>

proof end;

definition

let c₁ be non empty set ;
let c₂ be Element of c₁;
redefine func <% as <%c₂%> -> XFinSequence of a₁;
coherence

proof end;

end;

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

for b₁ being XFinSequence holds P₁[b₁]

provided

E31: P₁[ {} ] and
E32: for b₁ being XFinSequence
for b₂ being set st P₁[b₁] holds
P₁[b₁ ^ <%b₂%>]

proof end;

theorem Th45: :: AFINSQ_1:45

for b₁, b₂, b₃, b₄ being XFinSequence st b₁ ^ b₂ = b₃ ^ b₄ & len b₁ <= len b₃ holds
ex b₅ being XFinSequence st b₁ ^ b₅ = b₃

proof end;

definition

let c₁ be set ;
func c₁ ^omega -> set means :Def8: :: AFINSQ_1:def 8
for b₁ being set holds
( b₁ in a₂ iff b₁ is XFinSequence of a₁ );
existence

proof end;

uniqueness

proof end;

end;

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

registration

let c₁ be set ;
cluster a₁ ^omega -> non empty ;
coherence

proof end;

end;

theorem Th46: :: AFINSQ_1:46

for b₁, b₂ being set holds
( b₁ in b₂ ^omega iff b₁ is XFinSequence of b₂ ) by Def8;

theorem Th47: :: AFINSQ_1:47

for b₁ being set holds {} in b₁ ^omega

proof end;

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

ex b₁ being set st
for b₂ being set holds
( b₂ in b₁ iff ex b₃ being XFinSequence st
( b₃ in F₁() ^omega & P₁[b₃] & b₂ = b₃ ) )

proof end;

notation

let c₁ be XFinSequence;
let c₂, c₃ be set ;
synonym Replace c₁,c₂,c₃ for c₁ +* c₂,c₃;

end;

registration

let c₁ be XFinSequence;
let c₂, c₃ be set ;
cluster Replace a₁,a₂,a₃ -> T-Sequence-like finite ;
coherence

proof end;

end;

theorem Th48: :: AFINSQ_1:48

for b₁ being XFinSequence
for b₂ being Nat
for b₃ being set holds
( len (Replace b₁,b₂,b₃) = len b₁ & ( b₂ < len b₁ implies (Replace b₁,b₂,b₃) . b₂ = b₃ ) & ( for b₄ being Nat st b₄ <> b₂ holds
(Replace b₁,b₂,b₃) . b₄ = b₁ . b₄ ) )

proof end;

definition

let c₁ be non empty set ;
let c₂ be XFinSequence of c₁;
let c₃ be Nat;
let c₄ be Element of c₁;
redefine func Replace as Replace c₂,c₃,c₄ -> XFinSequence of a₁;
coherence

proof end;

end;