defpred S₁[ Element of 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 Element of 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 set 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 Element of 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 Element of 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 Element of NAT st n + 2 <= len p9 holds
p9 . (n + 2) = f . [n,(p9 . (n + 1))] ) & p = p9 ) by A4, A7;
A12: for n being Element of 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 Element of 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 Element of NAT by ORDINAL1:def 12;
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

let x be set ; :: 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, A22, A23, A25, A26;
hence x in q by A27, FUNCT_1:1; :: thesis: verum

end;

hence p c= q by TARSKI:def 3; :: thesis: verum

end;

ex f being Function st f = union X

proof

defpred S₃[ set , set ] means [$1,$2] in union X;
A28: for x, y, z being set st S₃[x,y] & S₃[x,z] holds
y = z

proof

let x, y, z be set ; :: thesis: ( S₃[x,y] & S₃[x,z] implies 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;

A35: now

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

end;

now

assume 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;

hence y = z by A35; :: thesis: verum

end;

consider h being Function such that
A37: for x, y being set holds
( [x,y] in h iff ( x in NAT & S₃[x,y] ) ) from FUNCT_1:sch 1(A28);
take h ; :: thesis: h = union X
A38: for x, y being set holds
( [x,y] in h iff [x,y] in union X )

proof

let x, y be set ; :: thesis: ( [x,y] in h iff [x,y] in union X )
thus ( [x,y] in h implies [x,y] in union X ) by A37; :: thesis: ( [x,y] in union X implies [x,y] in h )
thus ( [x,y] in union X implies [x,y] in h ) :: thesis: verum

proof

assume A39: [x,y] in union X ; :: thesis: [x,y] in h
then consider Z being set such that
A40: [x,y] in Z and
A41: Z in X by TARSKI:def 4;
Z in F₁() * by A5, A41;
then reconsider p = Z as FinSequence of F₁() by FINSEQ_1:def 11;
x in dom p by A40, RELAT_1:def 4;
hence [x,y] in h by A37, A39; :: thesis: verum

end;

end;

for x being set holds
( x in h iff x in union X )

proof

let x be set ; :: thesis: ( x in h iff x in union X )
thus ( x in h implies x in union X ) :: thesis: ( x in union X implies x in h )

proof

assume A42: x in h ; :: thesis: x in union X
then ex y, z being set st [y,z] = x by RELAT_1:def 1;
hence x in union X by A38, A42; :: thesis: verum

end;

assume A43: x in union X ; :: thesis: x in h
then consider Z being set such that
A44: x in Z and
A45: Z in X by TARSKI:def 4;
Z in F₁() * by A5, A45;
then reconsider p = Z as FinSequence of F₁() by FINSEQ_1:def 11;
x in p by A44;
then ex y, z being set st [y,z] = x by RELAT_1:def 1;
hence x in h by A38, A43; :: thesis: verum

end;

hence h = union X by TARSKI:1; :: thesis: verum

end;

then consider g being Function such that
A46: g = union X ;
A47: for x being set st x in rng g holds
x in F₁()

proof

let x be set ; :: thesis: ( x in rng g implies x in F₁() )
assume x in rng g ; :: thesis: x in F₁()
then consider y being set such that
A48: ( y in dom g & x = g . y ) by FUNCT_1:def 3;
[y,x] in union X by A46, A48, FUNCT_1:1;
then consider Z being set such that
A49: [y,x] in Z and
A50: Z in X by TARSKI:def 4;
Z in F₁() * by A5, A50;
then reconsider p = Z as FinSequence of F₁() by FINSEQ_1:def 11;
( y in dom p & x = p . y ) by A49, FUNCT_1:1;
then A51: x in rng p by FUNCT_1:def 3;
rng p c= F₁() by FINSEQ_1:def 4;
hence x in F₁() by A51; :: thesis: verum

end;

then rng g c= F₁() by TARSKI:def 3;
then reconsider h = g as Function of (dom g),F₁() by FUNCT_2:2;
A52: for n being Element of NAT holds n + 1 in dom h

proof

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

proof

let n be Element of 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 8, FINSEQ_1:def 11;
then <*F₂()*> in X by A4, A53;
then A54: {[1,F₂()]} in X by FINSEQ_1:37;
A55: for k being Element of NAT st S₃[k] holds
S₃[k + 1]

proof

let k be Element of 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 A46, FUNCT_1:1;
then consider Z being set such that
A56: [(k + 1),(h . (k + 1))] in Z and
A57: Z in X by TARSKI:def 4;
Z in F₁() * by A5, A57;
then reconsider Z = Z as FinSequence of F₁() by FINSEQ_1:def 11;
A58: ( k + 1 = len Z implies S₃[k + 1] )

proof

set p = Z ^ <*(f . [k,(Z . (k + 1))])*>;
A59: 1 <= (k + 1) + 1 by NAT_1:12;
assume A60: 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 A61: 1 in dom Z by FINSEQ_1:def 3;
A62: for n being Element of 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 Element of 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 A63: n + 2 <= (len Z) + (len <*(f . [k,(Z . (k + 1))])*>) by FINSEQ_1:22;
then A64: n + 2 <= (len Z) + 1 by FINSEQ_1:40;
A65: ( 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 A63, 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 A66: n + 1 in dom Z by FINSEQ_1:def 3;
A67: 1 <= n + (1 + 1) by NAT_1:12;
assume A68: 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 A64, NAT_1:8;
then n + 2 in Seg (len Z) by A67, FINSEQ_1:1;
then A69: n + 2 in dom Z by FINSEQ_1:def 3;
ex q being FinSequence st
( q in F₁() * & q . 1 = F₂() & ( for n being Element of NAT st n + 2 <= len q holds
q . (n + 2) = f . [n,(q . (n + 1))] ) & Z = q ) by A4, A57;
then Z . (n + 2) = f . [n,(Z . (n + 1))] by A64, A68, NAT_1:8;
then (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,(Z . (n + 1))] by A69, FINSEQ_1:def 7;
hence (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))] by A66, 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 A63, 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 A70: n + 1 in dom Z by FINSEQ_1:def 3;
assume A71: 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 A63, FINSEQ_1:23
.= f . [n,(Z . (n + 1))] by A60, A71, FINSEQ_1:40 ;
hence (Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 2) = f . [n,((Z ^ <*(f . [k,(Z . (k + 1))])*>) . (n + 1))] by A70, 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 A65; :: thesis: verum

end;

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

proof

1 <= k + 1 by NAT_1:12;
then k + 1 in Seg (len Z) by A60, FINSEQ_1:1;
then k + 1 in dom Z by FINSEQ_1:def 3;
then A73: 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 A73;
reconsider n = k as Element of NAT ;
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 A60, FINSEQ_1:39 ;
then (k + 1) + 1 in Seg (len (Z ^ <*(f . [k,(Z . (k + 1))])*>)) by A59, FINSEQ_1:1;
then (k + 1) + 1 in dom (Z ^ <*(f . [k,(Z . (k + 1))])*>) by FINSEQ_1:def 3;
then A74: [((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 Element of NAT st n + 2 <= len p holds
p . (n + 2) = f . [n,(p . (n + 1))] ) & Z = p ) by A4, A57;
then (Z ^ <*(f . [k,(Z . (k + 1))])*>) . 1 = F₂() by A61, FINSEQ_1:def 7;
then Z ^ <*(f . [k,(Z . (k + 1))])*> in X by A4, A72, A62;
then [((k + 1) + 1),((Z ^ <*(f . [k,(Z . (k + 1))])*>) . ((k + 1) + 1))] in h by A46, A74, 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 A56, FUNCT_1:1;
then k + 1 in Seg (len Z) by FINSEQ_1:def 3;
then A75: k + 1 <= len Z by FINSEQ_1:1;
assume k + 1 <> len Z ; :: thesis: S₃[k + 1]
then k + 1 < len Z by A75, XXREAL_0:1;
then A76: (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 A76, 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 A46, A57, TARSKI:def 4;
hence S₃[k + 1] by FUNCT_1:1; :: thesis: verum

end;

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

end;

[1,F₂()] in {[1,F₂()]} by TARSKI:def 1;
then [1,F₂()] in h by A46, A54, TARSKI:def 4;
then A77: S₃[ 0 ] by FUNCT_1:1;
thus for k being Element of NAT holds S₃[k] from NAT_1:sch 1(A77, A55); :: thesis: verum

end;

A78: for n being Element of NAT holds h . (n + 2) = f . [n,(h . (n + 1))]

proof

let n be Element of NAT ; :: thesis: h . (n + 2) = f . [n,(h . (n + 1))]
(n + 1) + 1 in dom h by A52;
then [(n + 2),(h . (n + 2))] in h by FUNCT_1:def 2;
then consider Z being set such that
A79: [(n + 2),(h . (n + 2))] in Z and
A80: Z in X by A46, TARSKI:def 4;
A81: ex p being FinSequence st
( p in F₁() * & p . 1 = F₂() & ( for n being Element of NAT st n + 2 <= len p holds
p . (n + 2) = f . [n,(p . (n + 1))] ) & Z = p ) by A4, A80;
Z in F₁() * by A5, A80;
then reconsider Z = Z as FinSequence of F₁() by FINSEQ_1:def 11;
n + 2 in dom Z by A79, FUNCT_1:1;
then n + 2 in Seg (len Z) by FINSEQ_1:def 3;
then A82: 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 A82, 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 A83: [(n + 1),(Z . (n + 1))] in h by A46, A80, TARSKI:def 4;
thus h . (n + 2) = Z . (n + 2) by A79, FUNCT_1:1
.= f . [n,(Z . (n + 1))] by A81, A82
.= f . [n,(h . (n + 1))] by A83, FUNCT_1:1 ; :: thesis: verum

end;

ex g being Function of NAT,F₁() st
for n being Element of NAT holds g . n = h . (n + 1)

proof

ex g being Function st
( dom g = NAT & ( for n being Element of NAT holds g . n = h . (n + 1) ) )

proof

defpred S₃[ set , set ] means ex n being Element of NAT st
( n = $1 & $2 = h . (n + 1) );
A84: for x being set st x in NAT holds
ex y being set st S₃[x,y]

proof

let x be set ; :: thesis: ( x in NAT implies ex y being set st S₃[x,y] )
assume x in NAT ; :: thesis: ex y being set st S₃[x,y]
then reconsider n = x as Element of 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
A85: ( dom g = NAT & ( for x being set st x in NAT holds
S₃[x,g . x] ) ) from CLASSES1:sch 1(A84);
take g ; :: thesis: ( dom g = NAT & ( for n being Element of NAT holds g . n = h . (n + 1) ) )
thus dom g = NAT by A85; :: thesis: for n being Element of NAT holds g . n = h . (n + 1)
thus for n being Element of NAT holds g . n = h . (n + 1) :: thesis: verum

proof

let n be Element of NAT ; :: thesis: g . n = h . (n + 1)
ex m being Element of NAT st
( m = n & g . n = h . (m + 1) ) by A85;
hence g . n = h . (n + 1) ; :: thesis: verum

end;

end;

then consider g being Function such that
A86: dom g = NAT and
A87: for n being Element of NAT holds g . n = h . (n + 1) ;
rng g c= F₁()

proof

let x be set ; :: 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 set such that
A88: y in dom g and
A89: x = g . y by FUNCT_1:def 3;
reconsider k = y as Element of NAT by A86, A88;
k + 1 in dom h by A52;
then A90: h . (k + 1) in rng h by FUNCT_1:def 3;
x = h . (k + 1) by A87, A89;
hence x in F₁() by A47, A90; :: thesis: verum

end;

then reconsider g = g as Function of NAT,F₁() by A86, FUNCT_2:2;
take g ; :: thesis: for n being Element of NAT holds g . n = h . (n + 1)
thus for n being Element of NAT holds g . n = h . (n + 1) by A87; :: thesis: verum

end;

then consider g being Function of NAT,F₁() such that
A91: for n being Element of NAT holds g . n = h . (n + 1) ;
A92: for n being Element of NAT st n + 2 <= len <*F₂()*> holds
<*F₂()*> . (n + 2) = f . [n,(<*F₂()*> . (n + 1))]

proof

let n be Element of 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 8, FINSEQ_1:def 11;
then <*F₂()*> in X by A4, A92;
then A93: {[1,F₂()]} in X by FINSEQ_1:37;
take g ; :: thesis: ( g . 0 = F₂() & ( for n being Element of NAT holds P₁[n,g . n,g . (n + 1)] ) )
[1,F₂()] in {[1,F₂()]} by TARSKI:def 1;
then [1,F₂()] in h by A46, A93, TARSKI:def 4;
then F₂() = h . (0 + 1) by FUNCT_1:1
.= g . 0 by A91 ;
hence g . 0 = F₂() ; :: thesis: for n being Element of NAT holds P₁[n,g . n,g . (n + 1)]
let n be Element of NAT ; :: thesis: P₁[n,g . n,g . (n + 1)]
A94: h . (n + (1 + 1)) = f . (n,(h . (n + 1))) by A78;
P₁[n,g . n,f . (n,(g . n))] by A3;
then P₁[n,g . n,h . ((n + 1) + 1)] by A91, A94;
hence P₁[n,g . n,g . (n + 1)] by A91; :: thesis: verum