defpred S1[ set , set , set ] means ( $2 is Function of F1(),F1() implies ex g1, g2 being Function of F1(),F1() st
( g1 = $2 & g2 = $3 & P1[$1,g1,g2] ) );
A2: for n being Nat
for x being set ex y being set st S1[n,x,y]
proof
let n be Nat; :: thesis: for x being set ex y being set st S1[n,x,y]
let x be set ; :: thesis: ex y being set st S1[n,x,y]
thus ex y being set st S1[n,x,y] :: thesis: verum
proof
per cases ( not x is Function of F1(),F1() or x is Function of F1(),F1() ) ;
suppose B0: x is not Function of F1(),F1() ; :: thesis: ex y being set st S1[n,x,y]
take y = 0 ; :: thesis: S1[n,x,y]
thus S1[n,x,y] by B0; :: thesis: verum
end;
suppose x is Function of F1(),F1() ; :: thesis: ex y being set st S1[n,x,y]
then reconsider g1 = x as Function of F1(),F1() ;
consider g2 being Function of F1(),F1() such that
B1: P1[n,g1,g2] by A1;
take y = g2; :: thesis: S1[n,x,y]
thus S1[n,x,y] by B1; :: thesis: verum
end;
end;
end;
end;
consider f being Function such that
A3: ( dom f = NAT & f . 0 = F2() & ( for n being Nat holds S1[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch 1(A2);
 reconsider f = f as sequence by A3, FIELD_12:def 2;
A4: for i being Nat holds f . i is Function of F1(),F1()
proof
let i be Nat; :: thesis: f . i is Function of F1(),F1()
defpred S2[ Nat] means f . $1 is Function of F1(),F1();
IA: S2[ 0 ] by A3;
IS: now :: thesis: for k being Nat st S2[k] holds
S2[k + 1]
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume IV: S2[k] ; :: thesis: S2[k + 1]
S1[k,f . k,f . (k + 1)] by A3;
hence S2[k + 1] by IV; :: thesis: verum
end;
for k being Nat holds S2[k] from NAT_1:sch 2(IA, IS);
 hence f . i is Function of F1(),F1() ; :: thesis: verum
end;
now :: thesis: for x being object st x in rng f holds
x in Funcs (F1(),F1())
let x be object ; :: thesis: ( x in rng f implies x in Funcs (F1(),F1()) )
assume x in rng f ; :: thesis: x in Funcs (F1(),F1())
then consider i being object such that
C1: ( i in dom f & f . i = x ) by FUNCT_1:def 3;
reconsider i = i as Element of NAT by C1;
reconsider g = x as Function of F1(),F1() by C1, A4;
( dom g = the carrier of F1() & rng g c= the carrier of F1() ) by FUNCT_2:def 1, RELAT_1:def 19;
hence x in Funcs (F1(),F1()) by FUNCT_2:def 2; :: thesis: verum
end;
then rng f c= Funcs (F1(),F1()) ;
then reconsider f = f as Funcs (F1(),F1()) -valued sequence by RELAT_1:def 19;
take f ; :: thesis: ( f . 0 = F2() & ( for n being Nat holds P1[n,f . n,f . (n + 1)] ) )
thus f . 0 = F2() by A3; :: thesis: for n being Nat holds P1[n,f . n,f . (n + 1)]
thus for n being Nat holds P1[n,f . n,f . (n + 1)] :: thesis: verum
proof
let n be Nat; :: thesis: P1[n,f . n,f . (n + 1)]
S1[n,f . n,f . (n + 1)] by A3;
hence P1[n,f . n,f . (n + 1)] ; :: thesis: verum
end;