defpred S₁[ Nat, set , set ] means P₁[$1,$2,$3];
A2: for x being Element of NAT
for y being Element of F₁() ex z being Element of F₁() st S₁[x,y,z] by A1;
consider f being Function of [:NAT,F₁():],F₁() such that
A3: for x being Element of NAT
for y being Element of F₁() holds S₁[x,y,f . (x,y)] from BINOP_1:sch 3(A2);
defpred S₂[ FinSequence] means ( $1 . 1 = F₂() & ( 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₁() * & S₂[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₁() *

proof

let x be set ; :: thesis: ( x in X implies x in F₁() * )
assume x in X ; :: thesis: x in F₁() *
then ex p being FinSequence st
( p in F₁() * & p . 1 = F₂() & ( 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₁() * ; :: thesis: verum

end;

A6: for p, q being FinSequence st p in X & q in X & len p <= len q holds
p c= q

proof

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₁() * & q9 . 1 = F₂() & ( 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₁() * & p9 . 1 = F₂() & ( 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

proof

defpred S₃[ Nat] means ( 1 <= $1 & $1 <= len p & p . $1 <> q . $1 );
assume ex n being Nat st S₃[n] ; :: thesis: contradiction
then A13: ex n being Nat st S₃[n] ;
consider k being Nat such that
A14: ( S₃[k] & ( for n being Nat st S₃[n] holds
k <= n ) ) from NAT_1:sch 5(A13);
k = 1

proof

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;

hence contradiction by A11, A10, A14; :: thesis: verum

end;

now :: thesis: for x being object st x in p holds
x 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;

hence p c= q ; :: thesis: verum

end;

A28: union X is Function-like

proof

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₁() * by A5, A32;
then reconsider q = Z2 as FinSequence of F₁() 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₁() * by A5, A34;
then reconsider p = Z1 as FinSequence of F₁() by FINSEQ_1:def 11;

per cases ( len q <= len p or len p <= len q ) ;

suppose len q <= len p ; :: thesis: y = z

then A35: q c= Z1 by A6, A34, A32;
[x,y] in p by A33;
hence y = z by A31, A35, FUNCT_1:def 1; :: thesis: verum

end;

suppose len p <= len q ; :: thesis: y = z

then p c= Z2 by A6, A34, A32;
then [x,y] in q by A33;
hence y = z by A31, FUNCT_1:def 1; :: thesis: verum

end;

end;

end;

union X is Relation-like

proof

let x be object ; :: according to RELAT_1:def 1 :: thesis: ( not x in union X or ex b₁, b₂ being object st x = [b₁,b₂] )
assume x in union X ; :: thesis: ex b₁, b₂ being object st x = [b₁,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₁() * & S₂[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;

then consider g being Function such that
A38: g = union X by A28;
A39: for x being object st x in rng g holds
x in F₁()

proof

let x be object ; :: thesis: ( x in rng g implies x in F₁() )
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₁() * by A5, A42;
then reconsider p = Z as FinSequence of F₁() 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₁() by FINSEQ_1:def 4;
hence x in F₁() by A43; :: thesis: verum

end;

then rng g c= F₁() ;
then reconsider h = g as Function of (dom g),F₁() by FUNCT_2:2;
A44: for n being Nat holds n + 1 in dom h

proof

defpred S₃[ Nat] means $1 + 1 in dom h;
A45: for n being Nat st n + 2 <= len <*F₂()*> holds
<*F₂()*> . (n + 2) = f . [n,(<*F₂()*> . (n + 1))]

proof

let n be Nat; :: thesis: ( n + 2 <= len <*F₂()*> implies <*F₂()*> . (n + 2) = f . [n,(<*F₂()*> . (n + 1))] )
assume n + 2 <= len <*F₂()*> ; :: thesis: <*F₂()*> . (n + 2) = f . [n,(<*F₂()*> . (n + 1))]
then n + 2 <= 1 by FINSEQ_1:39;
then n + (1 + 1) <= n + 1 by NAT_1:12;
hence <*F₂()*> . (n + 2) = f . [n,(<*F₂()*> . (n + 1))] by XREAL_1:6; :: thesis: verum

end;

( <*F₂()*> . 1 = F₂() & <*F₂()*> in F₁() * ) by FINSEQ_1:def 11;
then <*F₂()*> in X by A4, A45;
then A46: {[1,F₂()]} in X by FINSEQ_1:37;
A47: for k being Nat st S₃[k] holds
S₃[k + 1]

proof

let k be Nat; :: thesis: ( S₃[k] implies S₃[k + 1] )
assume k + 1 in dom h ; :: thesis: S₃[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₁() * by A5, A49;
then reconsider Z = Z as FinSequence of F₁() by FINSEQ_1:def 11;
A50: ( k + 1 = len Z implies S₃[k + 1] )

proof

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₃[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))]

proof

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))] )

proof

(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₁() * & q . 1 = F₂() & ( 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;

( 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 + 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 ;
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;

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

end;

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

proof

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₁() by FINSEQ_1:def 4;
then reconsider z = Z . (k + 1) as Element of F₁() 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₁() * by FINSEQ_1:def 11; :: thesis: verum

end;

len (Z ^ <*(f . [k,(Z . (k + 1))])*>) = (len Z) + (len <*(f . [k,(Z . (k + 1))])*>) by FINSEQ_1:22
.= (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 . 1 = F₂() & ( 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₂() 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₃[k + 1] by FUNCT_1:1; :: thesis: verum

end;

( k + 1 <> len Z implies S₃[k + 1] )

proof

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₃[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₃[k + 1] by FUNCT_1:1; :: thesis: verum

end;

hence S₃[k + 1] by A50; :: thesis: verum

end;

[1,F₂()] in {[1,F₂()]} by TARSKI:def 1;
then [1,F₂()] in h by A38, A46, TARSKI:def 4;
then A69: S₃[ 0 ] by FUNCT_1:1;
thus for k being Nat holds S₃[k] from NAT_1:sch 2(A69, A47); :: thesis: verum

end;

A70: for n being Nat holds h . (n + 2) = f . [n,(h . (n + 1))]

proof

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₁() * & p . 1 = F₂() & ( 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₁() * by A5, A72;
then reconsider Z = Z as FinSequence of F₁() 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;

defpred S₃[ 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₃[x,y]

proof

let x be object ; :: thesis: ( x in NAT implies ex y being object st S₃[x,y] )
assume x in NAT ; :: thesis: ex y being object st S₃[x,y]
then reconsider n = x as Nat ;
take h . (n + 1) ; :: thesis: S₃[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;

consider g being Function such that
A77: ( dom g = NAT & ( for x being object st x in NAT holds
S₃[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)

proof

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;

rng g c= F₁()

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng g or x in F₁() )
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₁() by A39, A82; :: thesis: verum

end;

then reconsider g = g as sequence of F₁() 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₂()*> holds
<*F₂()*> . (n + 2) = f . [n,(<*F₂()*> . (n + 1))]

proof

let n be Nat; :: thesis: ( n + 2 <= len <*F₂()*> implies <*F₂()*> . (n + 2) = f . [n,(<*F₂()*> . (n + 1))] )
assume n + 2 <= len <*F₂()*> ; :: thesis: <*F₂()*> . (n + 2) = f . [n,(<*F₂()*> . (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₂()*> . (n + 2) = f . [n,(<*F₂()*> . (n + 1))] by XREAL_1:6; :: thesis: verum

end;

( <*F₂()*> in F₁() * & <*F₂()*> . 1 = F₂() ) by FINSEQ_1:def 11;
then <*F₂()*> in X by A4, A84;
then A85: {[1,F₂()]} in X by FINSEQ_1:37;
take g ; :: thesis: ( g . 0 = F₂() & ( for n being Nat holds P₁[n,g . n,g . (n + 1)] ) )
[1,F₂()] in {[1,F₂()]} by TARSKI:def 1;
then [1,F₂()] in h by A38, A85, TARSKI:def 4;
then F₂() = h . (0 + 1) by FUNCT_1:1
.= g . 0 by A83 ;
hence g . 0 = F₂() ; :: thesis: for n being Nat holds P₁[n,g . n,g . (n + 1)]
let n be Nat; :: thesis: P₁[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₁() by FUNCT_2:5;
then P₁[n,g . n,f . (n,(g . n))] by A3, A87;
then P₁[n,g . n,h . ((n + 1) + 1)] by A83, A86;
hence P₁[n,g . n,g . (n + 1)] by A83; :: thesis: verum