defpred S_{1}[ Nat, set , set ] means P_{1}[$1,$2,$3];

A2: for x being Element of NAT

for y being Element of F_{1}() ex z being Element of F_{1}() st S_{1}[x,y,z]
by A1;

consider f being Function of [:NAT,F_{1}():],F_{1}() such that

A3: for x being Element of NAT

for y being Element of F_{1}() holds S_{1}[x,y,f . (x,y)]
from BINOP_1:sch 3(A2);

defpred S_{2}[ FinSequence] means ( $1 . 1 = F_{2}() & ( for n being Nat st n + 2 <= len $1 holds

$1 . (n + 2) = f . [n,($1 . (n + 1))] ) );

consider X being set such that

A4: for x being object holds

( x in X iff ex p being FinSequence st

( p in F_{1}() * & S_{2}[p] & x = p ) )
from FINSEQ_1:sch 4();

set Y = union X;

A5: for x being set st x in X holds

x in F_{1}() *

p c= q

A38: g = union X by A28;

A39: for x being object st x in rng g holds

x in F_{1}()
_{1}()
;

then reconsider h = g as Function of (dom g),F_{1}() by FUNCT_2:2;

A44: for n being Nat holds n + 1 in dom h_{3}[ object , object ] means ex n being Nat st

( n = $1 & $2 = h . (n + 1) );

A76: for x being object st x in NAT holds

ex y being object st S_{3}[x,y]

A77: ( dom g = NAT & ( for x being object st x in NAT holds

S_{3}[x,g . x] ) )
from CLASSES1:sch 1(A76);

A78: dom g = NAT by A77;

A79: for n being Nat holds g . n = h . (n + 1)_{1}()
_{1}() by A78, FUNCT_2:2;

A83: for n being Nat holds g . n = h . (n + 1) by A79;

A84: for n being Nat st n + 2 <= len <*F_{2}()*> holds

<*F_{2}()*> . (n + 2) = f . [n,(<*F_{2}()*> . (n + 1))]
_{2}()*> in F_{1}() * & <*F_{2}()*> . 1 = F_{2}() )
by FINSEQ_1:def 8, FINSEQ_1:def 11;

then <*F_{2}()*> in X
by A4, A84;

then A85: {[1,F_{2}()]} in X
by FINSEQ_1:37;

take g ; :: thesis: ( g . 0 = F_{2}() & ( for n being Nat holds P_{1}[n,g . n,g . (n + 1)] ) )

[1,F_{2}()] in {[1,F_{2}()]}
by TARSKI:def 1;

then [1,F_{2}()] in h
by A38, A85, TARSKI:def 4;

then F_{2}() =
h . (0 + 1)
by FUNCT_1:1

.= g . 0 by A83 ;

hence g . 0 = F_{2}()
; :: thesis: for n being Nat holds P_{1}[n,g . n,g . (n + 1)]

let n be Nat; :: thesis: P_{1}[n,g . n,g . (n + 1)]

A86: h . (n + (1 + 1)) = f . (n,(h . (n + 1))) by A70;

A87: n in NAT by ORDINAL1:def 12;

then g . n in F_{1}()
by FUNCT_2:5;

then P_{1}[n,g . n,f . (n,(g . n))]
by A3, A87;

then P_{1}[n,g . n,h . ((n + 1) + 1)]
by A83, A86;

hence P_{1}[n,g . n,g . (n + 1)]
by A83; :: thesis: verum

A2: for x being Element of NAT

for y being Element of F

consider f being Function of [:NAT,F

A3: for x being Element of NAT

for y being Element of F

defpred S

$1 . (n + 2) = f . [n,($1 . (n + 1))] ) );

consider X being set such that

A4: for x being object holds

( x in X iff ex p being FinSequence st

( p in F

set Y = union X;

A5: for x being set st x in X holds

x in F

proof

A6:
for p, q being FinSequence st p in X & q in X & len p <= len q holds
let x be set ; :: thesis: ( x in X implies x in F_{1}() * )

assume x in X ; :: thesis: x in F_{1}() *

then ex p being FinSequence st

( p in F_{1}() * & p . 1 = F_{2}() & ( for n being Nat st n + 2 <= len p holds

p . (n + 2) = f . [n,(p . (n + 1))] ) & x = p ) by A4;

hence x in F_{1}() *
; :: thesis: verum

end;assume x in X ; :: thesis: x in F

then ex p being FinSequence st

( p in F

p . (n + 2) = f . [n,(p . (n + 1))] ) & x = p ) by A4;

hence x in F

p c= q

proof

A28:
union X is Function-like
let p, q be FinSequence; :: thesis: ( p in X & q in X & len p <= len q implies p c= q )

assume that

A7: p in X and

A8: q in X and

A9: len p <= len q ; :: thesis: p c= q

A10: ex q9 being FinSequence st

( q9 in F_{1}() * & q9 . 1 = F_{2}() & ( for n being Nat st n + 2 <= len q9 holds

q9 . (n + 2) = f . [n,(q9 . (n + 1))] ) & q = q9 ) by A4, A8;

A11: ex p9 being FinSequence st

( p9 in F_{1}() * & p9 . 1 = F_{2}() & ( for n being Nat st n + 2 <= len p9 holds

p9 . (n + 2) = f . [n,(p9 . (n + 1))] ) & p = p9 ) by A4, A7;

A12: for n being Nat st 1 <= n & n <= len p holds

p . n = q . n

end;assume that

A7: p in X and

A8: q in X and

A9: len p <= len q ; :: thesis: p c= q

A10: ex q9 being FinSequence st

( q9 in F

q9 . (n + 2) = f . [n,(q9 . (n + 1))] ) & q = q9 ) by A4, A8;

A11: ex p9 being FinSequence st

( p9 in F

p9 . (n + 2) = f . [n,(p9 . (n + 1))] ) & p = p9 ) by A4, A7;

A12: for n being Nat st 1 <= n & n <= len p holds

p . n = q . n

proof

defpred S_{3}[ Nat] means ( 1 <= $1 & $1 <= len p & p . $1 <> q . $1 );

assume ex n being Nat st S_{3}[n]
; :: thesis: contradiction

then A13: ex n being Nat st S_{3}[n]
;

consider k being Nat such that

A14: ( S_{3}[k] & ( for n being Nat st S_{3}[n] holds

k <= n ) ) from NAT_1:sch 5(A13);

k = 1

end;assume ex n being Nat st S

then A13: ex n being Nat st S

consider k being Nat such that

A14: ( S

k <= n ) ) from NAT_1:sch 5(A13);

k = 1

proof

hence
contradiction
by A11, A10, A14; :: thesis: verum
0 <> k
by A14;

then consider n being Nat such that

A15: k = n + 1 by NAT_1:6;

n + 0 <= n + 1 by XREAL_1:7;

then A16: n <= len p by A14, A15, XXREAL_0:2;

A17: n + 0 < n + 1 by XREAL_1:6;

assume A18: k <> 1 ; :: thesis: contradiction

then 1 < n + 1 by A14, A15, XXREAL_0:1;

then A19: 1 <= n by NAT_1:13;

n <> 0 by A18, A15;

then consider m being Nat such that

A20: n = m + 1 by NAT_1:6;

reconsider m = m as Nat ;

A21: m + 2 <= len q by A9, A14, A15, A20, XXREAL_0:2;

p . k = p . (m + (1 + 1)) by A15, A20

.= f . [m,(p . n)] by A11, A14, A15, A20

.= f . [m,(q . (m + 1))] by A14, A15, A19, A16, A17, A20

.= q . k by A10, A15, A20, A21 ;

hence contradiction by A14; :: thesis: verum

end;then consider n being Nat such that

A15: k = n + 1 by NAT_1:6;

n + 0 <= n + 1 by XREAL_1:7;

then A16: n <= len p by A14, A15, XXREAL_0:2;

A17: n + 0 < n + 1 by XREAL_1:6;

assume A18: k <> 1 ; :: thesis: contradiction

then 1 < n + 1 by A14, A15, XXREAL_0:1;

then A19: 1 <= n by NAT_1:13;

n <> 0 by A18, A15;

then consider m being Nat such that

A20: n = m + 1 by NAT_1:6;

reconsider m = m as Nat ;

A21: m + 2 <= len q by A9, A14, A15, A20, XXREAL_0:2;

p . k = p . (m + (1 + 1)) by A15, A20

.= f . [m,(p . n)] by A11, A14, A15, A20

.= f . [m,(q . (m + 1))] by A14, A15, A19, A16, A17, A20

.= q . k by A10, A15, A20, A21 ;

hence contradiction by A14; :: thesis: verum

now :: thesis: for x being object st x in p holds

x in q

hence
p c= q
; :: thesis: verumx in q

let x be object ; :: thesis: ( x in p implies x in q )

assume x in p ; :: thesis: x in q

then consider n being Nat such that

A22: n in dom p and

A23: x = [n,(p . n)] by FINSEQ_1:12;

A24: n in Seg (len p) by A22, FINSEQ_1:def 3;

then A25: 1 <= n by FINSEQ_1:1;

A26: n <= len p by A24, FINSEQ_1:1;

then n <= len q by A9, XXREAL_0:2;

then n in Seg (len q) by A25, FINSEQ_1:1;

then A27: n in dom q by FINSEQ_1:def 3;

x = [n,(q . n)] by A12, A23, A25, A26;

hence x in q by A27, FUNCT_1:1; :: thesis: verum

end;assume x in p ; :: thesis: x in q

then consider n being Nat such that

A22: n in dom p and

A23: x = [n,(p . n)] by FINSEQ_1:12;

A24: n in Seg (len p) by A22, FINSEQ_1:def 3;

then A25: 1 <= n by FINSEQ_1:1;

A26: n <= len p by A24, FINSEQ_1:1;

then n <= len q by A9, XXREAL_0:2;

then n in Seg (len q) by A25, FINSEQ_1:1;

then A27: n in dom q by FINSEQ_1:def 3;

x = [n,(q . n)] by A12, A23, A25, A26;

hence x in q by A27, FUNCT_1:1; :: thesis: verum

proof

union X is Relation-like
let x, y, z be object ; :: according to FUNCT_1:def 1 :: thesis: ( not [x,y] in union X or not [x,z] in union X or y = z )

assume that

A29: [x,y] in union X and

A30: [x,z] in union X ; :: thesis: y = z

consider Z2 being set such that

A31: [x,z] in Z2 and

A32: Z2 in X by A30, TARSKI:def 4;

Z2 in F_{1}() *
by A5, A32;

then reconsider q = Z2 as FinSequence of F_{1}() by FINSEQ_1:def 11;

consider Z1 being set such that

A33: [x,y] in Z1 and

A34: Z1 in X by A29, TARSKI:def 4;

Z1 in F_{1}() *
by A5, A34;

then reconsider p = Z1 as FinSequence of F_{1}() by FINSEQ_1:def 11;

end;assume that

A29: [x,y] in union X and

A30: [x,z] in union X ; :: thesis: y = z

consider Z2 being set such that

A31: [x,z] in Z2 and

A32: Z2 in X by A30, TARSKI:def 4;

Z2 in F

then reconsider q = Z2 as FinSequence of F

consider Z1 being set such that

A33: [x,y] in Z1 and

A34: Z1 in X by A29, TARSKI:def 4;

Z1 in F

then reconsider p = Z1 as FinSequence of F

proof

then consider g being Function such that
let x be object ; :: according to RELAT_1:def 1 :: thesis: ( not x in union X or ex b_{1}, b_{2} being object st x = [b_{1},b_{2}] )

assume x in union X ; :: thesis: ex b_{1}, b_{2} being object st x = [b_{1},b_{2}]

then consider Z2 being set such that

A36: x in Z2 and

A37: Z2 in X by TARSKI:def 4;

ex p being FinSequence st

( p in F_{1}() * & S_{2}[p] & Z2 = p )
by A4, A37;

then Z2 is Relation-like ;

hence ex y, z being object st x = [y,z] by A36; :: thesis: verum

end;assume x in union X ; :: thesis: ex b

then consider Z2 being set such that

A36: x in Z2 and

A37: Z2 in X by TARSKI:def 4;

ex p being FinSequence st

( p in F

then Z2 is Relation-like ;

hence ex y, z being object st x = [y,z] by A36; :: thesis: verum

A38: g = union X by A28;

A39: for x being object st x in rng g holds

x in F

proof

then
rng g c= F
let x be object ; :: thesis: ( x in rng g implies x in F_{1}() )

assume x in rng g ; :: thesis: x in F_{1}()

then consider y being object such that

A40: ( y in dom g & x = g . y ) by FUNCT_1:def 3;

[y,x] in union X by A38, A40, FUNCT_1:1;

then consider Z being set such that

A41: [y,x] in Z and

A42: Z in X by TARSKI:def 4;

Z in F_{1}() *
by A5, A42;

then reconsider p = Z as FinSequence of F_{1}() by FINSEQ_1:def 11;

( y in dom p & x = p . y ) by A41, FUNCT_1:1;

then A43: x in rng p by FUNCT_1:def 3;

rng p c= F_{1}()
by FINSEQ_1:def 4;

hence x in F_{1}()
by A43; :: thesis: verum

end;assume x in rng g ; :: thesis: x in F

then consider y being object such that

A40: ( y in dom g & x = g . y ) by FUNCT_1:def 3;

[y,x] in union X by A38, A40, FUNCT_1:1;

then consider Z being set such that

A41: [y,x] in Z and

A42: Z in X by TARSKI:def 4;

Z in F

then reconsider p = Z as FinSequence of F

( y in dom p & x = p . y ) by A41, FUNCT_1:1;

then A43: x in rng p by FUNCT_1:def 3;

rng p c= F

hence x in F

then reconsider h = g as Function of (dom g),F

A44: for n being Nat holds n + 1 in dom h

proof

A70:
for n being Nat holds h . (n + 2) = f . [n,(h . (n + 1))]
defpred S_{3}[ Nat] means $1 + 1 in dom h;

A45: for n being Nat st n + 2 <= len <*F_{2}()*> holds

<*F_{2}()*> . (n + 2) = f . [n,(<*F_{2}()*> . (n + 1))]
_{2}()*> . 1 = F_{2}() & <*F_{2}()*> in F_{1}() * )
by FINSEQ_1:def 8, FINSEQ_1:def 11;

then <*F_{2}()*> in X
by A4, A45;

then A46: {[1,F_{2}()]} in X
by FINSEQ_1:37;

A47: for k being Nat st S_{3}[k] holds

S_{3}[k + 1]
_{2}()] in {[1,F_{2}()]}
by TARSKI:def 1;

then [1,F_{2}()] in h
by A38, A46, TARSKI:def 4;

then A69: S_{3}[ 0 ]
by FUNCT_1:1;

thus for k being Nat holds S_{3}[k]
from NAT_1:sch 2(A69, A47); :: thesis: verum

end;A45: for n being Nat st n + 2 <= len <*F

<*F

proof

( <*F
let n be Nat; :: thesis: ( n + 2 <= len <*F_{2}()*> implies <*F_{2}()*> . (n + 2) = f . [n,(<*F_{2}()*> . (n + 1))] )

assume n + 2 <= len <*F_{2}()*>
; :: thesis: <*F_{2}()*> . (n + 2) = f . [n,(<*F_{2}()*> . (n + 1))]

then n + 2 <= 1 by FINSEQ_1:39;

then n + (1 + 1) <= n + 1 by NAT_1:12;

hence <*F_{2}()*> . (n + 2) = f . [n,(<*F_{2}()*> . (n + 1))]
by XREAL_1:6; :: thesis: verum

end;assume n + 2 <= len <*F

then n + 2 <= 1 by FINSEQ_1:39;

then n + (1 + 1) <= n + 1 by NAT_1:12;

hence <*F

then <*F

then A46: {[1,F

A47: for k being Nat st S

S

proof

[1,F
let k be Nat; :: thesis: ( S_{3}[k] implies S_{3}[k + 1] )

assume k + 1 in dom h ; :: thesis: S_{3}[k + 1]

then [(k + 1),(h . (k + 1))] in union X by A38, FUNCT_1:1;

then consider Z being set such that

A48: [(k + 1),(h . (k + 1))] in Z and

A49: Z in X by TARSKI:def 4;

Z in F_{1}() *
by A5, A49;

then reconsider Z = Z as FinSequence of F_{1}() by FINSEQ_1:def 11;

A50: ( k + 1 = len Z implies S_{3}[k + 1] )
_{3}[k + 1] )
_{3}[k + 1]
by A50; :: thesis: verum

end;assume k + 1 in dom h ; :: thesis: S

then [(k + 1),(h . (k + 1))] in union X by A38, FUNCT_1:1;

then consider Z being set such that

A48: [(k + 1),(h . (k + 1))] in Z and

A49: Z in X by TARSKI:def 4;

Z in F

then reconsider Z = Z as FinSequence of F

A50: ( k + 1 = len Z implies S

proof

( k + 1 <> len Z implies S
set p = Z ^ <*(f . [k,(Z . (k + 1))])*>;

A51: 1 <= (k + 1) + 1 by NAT_1:12;

assume A52: k + 1 = len Z ; :: thesis: S_{3}[k + 1]

then 1 <= len Z by NAT_1:12;

then 1 in Seg (len Z) by FINSEQ_1:1;

then A53: 1 in dom Z by FINSEQ_1:def 3;

A54: for n being Nat st n + 2 <= len (Z ^ <*(f . [k,(Z . (k + 1))])*>) holds

(Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))]_{1}() *

.= (k + 1) + 1 by A52, FINSEQ_1:39 ;

then (k + 1) + 1 in Seg (len (Z ^ <*(f . [k,(Z . (k + 1))])*>)) by A51, FINSEQ_1:1;

then (k + 1) + 1 in dom (Z ^ <*(f . [k,(Z . (k + 1))])*>) by FINSEQ_1:def 3;

then A66: [((k + 1) + 1),((Z ^ <*(f . [k,(Z . (k + 1))])*>) . ((k + 1) + 1))] in Z ^ <*(f . [k,(Z . (k + 1))])*> by FUNCT_1:1;

ex p being FinSequence st

( p in F_{1}() * & p . 1 = F_{2}() & ( for n being Nat st n + 2 <= len p holds

p . (n + 2) = f . [n,(p . (n + 1))] ) & Z = p ) by A4, A49;

then (Z ^ <*(f . [k,(Z . (k + 1))])*>) . 1 = F_{2}()
by A53, FINSEQ_1:def 7;

then Z ^ <*(f . [k,(Z . (k + 1))])*> in X by A4, A64, A54;

then [((k + 1) + 1),((Z ^ <*(f . [k,(Z . (k + 1))])*>) . ((k + 1) + 1))] in h by A38, A66, TARSKI:def 4;

hence S_{3}[k + 1]
by FUNCT_1:1; :: thesis: verum

end;A51: 1 <= (k + 1) + 1 by NAT_1:12;

assume A52: k + 1 = len Z ; :: thesis: S

then 1 <= len Z by NAT_1:12;

then 1 in Seg (len Z) by FINSEQ_1:1;

then A53: 1 in dom Z by FINSEQ_1:def 3;

A54: for n being Nat st n + 2 <= len (Z ^ <*(f . [k,(Z . (k + 1))])*>) holds

(Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))]

proof

A64:
Z ^ <*(f . [k,(Z . (k + 1))])*> in F
let n be Nat; :: thesis: ( n + 2 <= len (Z ^ <*(f . [k,(Z . (k + 1))])*>) implies (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))] )

assume n + 2 <= len (Z ^ <*(f . [k,(Z . (k + 1))])*>) ; :: thesis: (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))]

then A55: n + 2 <= (len Z) + (len <*(f . [k,(Z . (k + 1))])*>) by FINSEQ_1:22;

then A56: n + 2 <= (len Z) + 1 by FINSEQ_1:40;

A57: ( n + 2 <> (len Z) + 1 implies (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))] )

end;assume n + 2 <= len (Z ^ <*(f . [k,(Z . (k + 1))])*>) ; :: thesis: (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))]

then A55: n + 2 <= (len Z) + (len <*(f . [k,(Z . (k + 1))])*>) by FINSEQ_1:22;

then A56: n + 2 <= (len Z) + 1 by FINSEQ_1:40;

A57: ( n + 2 <> (len Z) + 1 implies (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))] )

proof

( n + 2 = (len Z) + 1 implies (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))] )
(n + 1) + 1 <= (len Z) + 1
by A55, FINSEQ_1:40;

then ( 1 <= n + 1 & n + 1 <= len Z ) by NAT_1:12, XREAL_1:6;

then n + 1 in Seg (len Z) by FINSEQ_1:1;

then A58: n + 1 in dom Z by FINSEQ_1:def 3;

A59: 1 <= n + (1 + 1) by NAT_1:12;

assume A60: n + 2 <> (len Z) + 1 ; :: thesis: (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))]

then n + 2 <= len Z by A56, NAT_1:8;

then n + 2 in Seg (len Z) by A59, FINSEQ_1:1;

then A61: n + 2 in dom Z by FINSEQ_1:def 3;

ex q being FinSequence st

( q in F_{1}() * & q . 1 = F_{2}() & ( for n being Nat st n + 2 <= len q holds

q . (n + 2) = f . [n,(q . (n + 1))] ) & Z = q ) by A4, A49;

then Z . (n + 2) = f . [n,(Z . (n + 1))] by A56, A60, NAT_1:8;

then (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,(Z . (n + 1))] by A61, FINSEQ_1:def 7;

hence (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))] by A58, FINSEQ_1:def 7; :: thesis: verum

end;then ( 1 <= n + 1 & n + 1 <= len Z ) by NAT_1:12, XREAL_1:6;

then n + 1 in Seg (len Z) by FINSEQ_1:1;

then A58: n + 1 in dom Z by FINSEQ_1:def 3;

A59: 1 <= n + (1 + 1) by NAT_1:12;

assume A60: n + 2 <> (len Z) + 1 ; :: thesis: (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))]

then n + 2 <= len Z by A56, NAT_1:8;

then n + 2 in Seg (len Z) by A59, FINSEQ_1:1;

then A61: n + 2 in dom Z by FINSEQ_1:def 3;

ex q being FinSequence st

( q in F

q . (n + 2) = f . [n,(q . (n + 1))] ) & Z = q ) by A4, A49;

then Z . (n + 2) = f . [n,(Z . (n + 1))] by A56, A60, NAT_1:8;

then (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,(Z . (n + 1))] by A61, FINSEQ_1:def 7;

hence (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))] by A58, FINSEQ_1:def 7; :: thesis: verum

proof

hence
(Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))]
by A57; :: thesis: verum
(n + 1) + 1 <= (len Z) + 1
by A55, FINSEQ_1:40;

then ( 1 <= n + 1 & n + 1 <= len Z ) by NAT_1:12, XREAL_1:6;

then n + 1 in Seg (len Z) by FINSEQ_1:1;

then A62: n + 1 in dom Z by FINSEQ_1:def 3;

assume A63: n + 2 = (len Z) + 1 ; :: thesis: (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))]

then (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = <*(f . [k,(Z . (k + 1))])*> . ((n + 2) - ((n + 2) - 1)) by A55, FINSEQ_1:23

.= f . [n,(Z . (n + 1))] by A52, A63, FINSEQ_1:40 ;

hence (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))] by A62, FINSEQ_1:def 7; :: thesis: verum

end;then ( 1 <= n + 1 & n + 1 <= len Z ) by NAT_1:12, XREAL_1:6;

then n + 1 in Seg (len Z) by FINSEQ_1:1;

then A62: n + 1 in dom Z by FINSEQ_1:def 3;

assume A63: n + 2 = (len Z) + 1 ; :: thesis: (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))]

then (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = <*(f . [k,(Z . (k + 1))])*> . ((n + 2) - ((n + 2) - 1)) by A55, FINSEQ_1:23

.= f . [n,(Z . (n + 1))] by A52, A63, FINSEQ_1:40 ;

hence (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))] by A62, FINSEQ_1:def 7; :: thesis: verum

proof

len (Z ^ <*(f . [k,(Z . (k + 1))])*>) =
(len Z) + (len <*(f . [k,(Z . (k + 1))])*>)
by FINSEQ_1:22
1 <= k + 1
by NAT_1:12;

then k + 1 in Seg (len Z) by A52, FINSEQ_1:1;

then k + 1 in dom Z by FINSEQ_1:def 3;

then A65: Z . (k + 1) in rng Z by FUNCT_1:def 3;

rng Z c= F_{1}()
by FINSEQ_1:def 4;

then reconsider z = Z . (k + 1) as Element of F_{1}() by A65;

reconsider n = k as Element of NAT by ORDINAL1:def 12;

Z ^ <*(f . [k,(Z . (k + 1))])*> = Z ^ <*(f . [n,z])*> ;

hence Z ^ <*(f . [k,(Z . (k + 1))])*> in F_{1}() *
by FINSEQ_1:def 11; :: thesis: verum

end;then k + 1 in Seg (len Z) by A52, FINSEQ_1:1;

then k + 1 in dom Z by FINSEQ_1:def 3;

then A65: Z . (k + 1) in rng Z by FUNCT_1:def 3;

rng Z c= F

then reconsider z = Z . (k + 1) as Element of F

reconsider n = k as Element of NAT by ORDINAL1:def 12;

Z ^ <*(f . [k,(Z . (k + 1))])*> = Z ^ <*(f . [n,z])*> ;

hence Z ^ <*(f . [k,(Z . (k + 1))])*> in F

.= (k + 1) + 1 by A52, FINSEQ_1:39 ;

then (k + 1) + 1 in Seg (len (Z ^ <*(f . [k,(Z . (k + 1))])*>)) by A51, FINSEQ_1:1;

then (k + 1) + 1 in dom (Z ^ <*(f . [k,(Z . (k + 1))])*>) by FINSEQ_1:def 3;

then A66: [((k + 1) + 1),((Z ^ <*(f . [k,(Z . (k + 1))])*>) . ((k + 1) + 1))] in Z ^ <*(f . [k,(Z . (k + 1))])*> by FUNCT_1:1;

ex p being FinSequence st

( p in F

p . (n + 2) = f . [n,(p . (n + 1))] ) & Z = p ) by A4, A49;

then (Z ^ <*(f . [k,(Z . (k + 1))])*>) . 1 = F

then Z ^ <*(f . [k,(Z . (k + 1))])*> in X by A4, A64, A54;

then [((k + 1) + 1),((Z ^ <*(f . [k,(Z . (k + 1))])*>) . ((k + 1) + 1))] in h by A38, A66, TARSKI:def 4;

hence S

proof

hence
S
k + 1 in dom Z
by A48, FUNCT_1:1;

then k + 1 in Seg (len Z) by FINSEQ_1:def 3;

then A67: k + 1 <= len Z by FINSEQ_1:1;

assume k + 1 <> len Z ; :: thesis: S_{3}[k + 1]

then k + 1 < len Z by A67, XXREAL_0:1;

then A68: (k + 1) + 1 <= len Z by NAT_1:13;

1 <= (k + 1) + 1 by NAT_1:12;

then (k + 1) + 1 in Seg (len Z) by A68, FINSEQ_1:1;

then (k + 1) + 1 in dom Z by FINSEQ_1:def 3;

then [((k + 1) + 1),(Z . ((k + 1) + 1))] in Z by FUNCT_1:1;

then [((k + 1) + 1),(Z . ((k + 1) + 1))] in h by A38, A49, TARSKI:def 4;

hence S_{3}[k + 1]
by FUNCT_1:1; :: thesis: verum

end;then k + 1 in Seg (len Z) by FINSEQ_1:def 3;

then A67: k + 1 <= len Z by FINSEQ_1:1;

assume k + 1 <> len Z ; :: thesis: S

then k + 1 < len Z by A67, XXREAL_0:1;

then A68: (k + 1) + 1 <= len Z by NAT_1:13;

1 <= (k + 1) + 1 by NAT_1:12;

then (k + 1) + 1 in Seg (len Z) by A68, FINSEQ_1:1;

then (k + 1) + 1 in dom Z by FINSEQ_1:def 3;

then [((k + 1) + 1),(Z . ((k + 1) + 1))] in Z by FUNCT_1:1;

then [((k + 1) + 1),(Z . ((k + 1) + 1))] in h by A38, A49, TARSKI:def 4;

hence S

then [1,F

then A69: S

thus for k being Nat holds S

proof

defpred S
let n be Nat; :: thesis: h . (n + 2) = f . [n,(h . (n + 1))]

(n + 1) + 1 in dom h by A44;

then [(n + 2),(h . (n + 2))] in h by FUNCT_1:def 2;

then consider Z being set such that

A71: [(n + 2),(h . (n + 2))] in Z and

A72: Z in X by A38, TARSKI:def 4;

A73: ex p being FinSequence st

( p in F_{1}() * & p . 1 = F_{2}() & ( for n being Nat st n + 2 <= len p holds

p . (n + 2) = f . [n,(p . (n + 1))] ) & Z = p ) by A4, A72;

Z in F_{1}() *
by A5, A72;

then reconsider Z = Z as FinSequence of F_{1}() by FINSEQ_1:def 11;

n + 2 in dom Z by A71, FUNCT_1:1;

then n + 2 in Seg (len Z) by FINSEQ_1:def 3;

then A74: n + 2 <= len Z by FINSEQ_1:1;

n + 1 <= n + 2 by XREAL_1:7;

then ( 1 <= n + 1 & n + 1 <= len Z ) by A74, NAT_1:12, XXREAL_0:2;

then n + 1 in Seg (len Z) by FINSEQ_1:1;

then n + 1 in dom Z by FINSEQ_1:def 3;

then [(n + 1),(Z . (n + 1))] in Z by FUNCT_1:1;

then A75: [(n + 1),(Z . (n + 1))] in h by A38, A72, TARSKI:def 4;

thus h . (n + 2) = Z . (n + 2) by A71, FUNCT_1:1

.= f . [n,(Z . (n + 1))] by A73, A74

.= f . [n,(h . (n + 1))] by A75, FUNCT_1:1 ; :: thesis: verum

end;(n + 1) + 1 in dom h by A44;

then [(n + 2),(h . (n + 2))] in h by FUNCT_1:def 2;

then consider Z being set such that

A71: [(n + 2),(h . (n + 2))] in Z and

A72: Z in X by A38, TARSKI:def 4;

A73: ex p being FinSequence st

( p in F

p . (n + 2) = f . [n,(p . (n + 1))] ) & Z = p ) by A4, A72;

Z in F

then reconsider Z = Z as FinSequence of F

n + 2 in dom Z by A71, FUNCT_1:1;

then n + 2 in Seg (len Z) by FINSEQ_1:def 3;

then A74: n + 2 <= len Z by FINSEQ_1:1;

n + 1 <= n + 2 by XREAL_1:7;

then ( 1 <= n + 1 & n + 1 <= len Z ) by A74, NAT_1:12, XXREAL_0:2;

then n + 1 in Seg (len Z) by FINSEQ_1:1;

then n + 1 in dom Z by FINSEQ_1:def 3;

then [(n + 1),(Z . (n + 1))] in Z by FUNCT_1:1;

then A75: [(n + 1),(Z . (n + 1))] in h by A38, A72, TARSKI:def 4;

thus h . (n + 2) = Z . (n + 2) by A71, FUNCT_1:1

.= f . [n,(Z . (n + 1))] by A73, A74

.= f . [n,(h . (n + 1))] by A75, FUNCT_1:1 ; :: thesis: verum

( n = $1 & $2 = h . (n + 1) );

A76: for x being object st x in NAT holds

ex y being object st S

proof

consider g being Function such that
let x be object ; :: thesis: ( x in NAT implies ex y being object st S_{3}[x,y] )

assume x in NAT ; :: thesis: ex y being object st S_{3}[x,y]

then reconsider n = x as Nat ;

take h . (n + 1) ; :: thesis: S_{3}[x,h . (n + 1)]

take n ; :: thesis: ( n = x & h . (n + 1) = h . (n + 1) )

thus ( n = x & h . (n + 1) = h . (n + 1) ) ; :: thesis: verum

end;assume x in NAT ; :: thesis: ex y being object st S

then reconsider n = x as Nat ;

take h . (n + 1) ; :: thesis: S

take n ; :: thesis: ( n = x & h . (n + 1) = h . (n + 1) )

thus ( n = x & h . (n + 1) = h . (n + 1) ) ; :: thesis: verum

A77: ( dom g = NAT & ( for x being object st x in NAT holds

S

A78: dom g = NAT by A77;

A79: for n being Nat holds g . n = h . (n + 1)

proof

rng g c= F
let n be Nat; :: thesis: g . n = h . (n + 1)

n in NAT by ORDINAL1:def 12;

then ex m being Nat st

( m = n & g . n = h . (m + 1) ) by A77;

hence g . n = h . (n + 1) ; :: thesis: verum

end;n in NAT by ORDINAL1:def 12;

then ex m being Nat st

( m = n & g . n = h . (m + 1) ) by A77;

hence g . n = h . (n + 1) ; :: thesis: verum

proof

then reconsider g = g as sequence of F
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng g or x in F_{1}() )

assume x in rng g ; :: thesis: x in F_{1}()

then consider y being object such that

A80: y in dom g and

A81: x = g . y by FUNCT_1:def 3;

reconsider k = y as Nat by A78, A80;

k + 1 in dom h by A44;

then A82: h . (k + 1) in rng h by FUNCT_1:def 3;

x = h . (k + 1) by A79, A81;

hence x in F_{1}()
by A39, A82; :: thesis: verum

end;assume x in rng g ; :: thesis: x in F

then consider y being object such that

A80: y in dom g and

A81: x = g . y by FUNCT_1:def 3;

reconsider k = y as Nat by A78, A80;

k + 1 in dom h by A44;

then A82: h . (k + 1) in rng h by FUNCT_1:def 3;

x = h . (k + 1) by A79, A81;

hence x in F

A83: for n being Nat holds g . n = h . (n + 1) by A79;

A84: for n being Nat st n + 2 <= len <*F

<*F

proof

( <*F
let n be Nat; :: thesis: ( n + 2 <= len <*F_{2}()*> implies <*F_{2}()*> . (n + 2) = f . [n,(<*F_{2}()*> . (n + 1))] )

assume n + 2 <= len <*F_{2}()*>
; :: thesis: <*F_{2}()*> . (n + 2) = f . [n,(<*F_{2}()*> . (n + 1))]

then (n + 1) + 1 <= 0 + 1 by FINSEQ_1:39;

then n + 1 <= 0 by XREAL_1:6;

then n + 1 <= 0 + n ;

hence <*F_{2}()*> . (n + 2) = f . [n,(<*F_{2}()*> . (n + 1))]
by XREAL_1:6; :: thesis: verum

end;assume n + 2 <= len <*F

then (n + 1) + 1 <= 0 + 1 by FINSEQ_1:39;

then n + 1 <= 0 by XREAL_1:6;

then n + 1 <= 0 + n ;

hence <*F

then <*F

then A85: {[1,F

take g ; :: thesis: ( g . 0 = F

[1,F

then [1,F

then F

.= g . 0 by A83 ;

hence g . 0 = F

let n be Nat; :: thesis: P

A86: h . (n + (1 + 1)) = f . (n,(h . (n + 1))) by A70;

A87: n in NAT by ORDINAL1:def 12;

then g . n in F

then P

then P

hence P