consider Y being set such that
A3: for x being object holds
( x in Y iff ( x in F1() & P1[x] ) ) from XBOOLE_0:sch 1();
 defpred S1[ object , object ] means ( $2 in Y & P2[$1,$2] );
A4: for x being object st x in Y holds
ex y being object st S1[x,y]
proof
let x be object ; :: thesis: ( x in Y implies ex y being object st S1[x,y] )
assume x in Y ; :: thesis: ex y being object st S1[x,y]
then ( x in F1() & P1[x] ) by A3;
then consider y being object such that
A5: ( y in F1() & P2[x,y] & P1[y] ) by A2;
take y ; :: thesis: S1[x,y]
thus S1[x,y] by A3, A5; :: thesis: verum
end;
consider g being Function such that
A6: ( dom g = Y & ( for x being object st x in Y holds
S1[x,g . x] ) ) from CLASSES1:sch 1(A4);
 deffunc H1( set , set ) -> set = g . $2;
consider f being Function such that
A7: ( dom f = NAT & f . 0 = F2() & ( for n being Nat holds f . (n + 1) = H1(n,f . n) ) ) from NAT_1:sch 11();
 take f ; :: thesis: ( dom f = NAT & rng f c= F1() & f . 0 = F2() & ( for k being Nat holds
( P2[f . k,f . (k + 1)] & P1[f . k] ) ) )
thus dom f = NAT by A7; :: thesis: ( rng f c= F1() & f . 0 = F2() & ( for k being Nat holds
( P2[f . k,f . (k + 1)] & P1[f . k] ) ) )
defpred S2[ Nat] means f . $1 in Y;
A8: S2[ 0 ] by A1, A3, A7;
A9: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
assume f . k in Y ; :: thesis: S2[k + 1]
then g . (f . k) in Y by A6;
hence S2[k + 1] by A7; :: thesis: verum
end;
A10: for k being Nat holds S2[k] from NAT_1:sch 2(A8, A9);
 thus rng f c= F1() :: thesis: ( f . 0 = F2() & ( for k being Nat holds
( P2[f . k,f . (k + 1)] & P1[f . k] ) ) )
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in F1() )
assume x in rng f ; :: thesis: x in F1()
then consider y being object such that
A11: y in dom f and
A12: x = f . y by FUNCT_1:def 3;
reconsider y = y as Nat by A7, A11;
f . y in Y by A10;
hence x in F1() by A3, A12; :: thesis: verum
end;
thus f . 0 = F2() by A7; :: thesis: for k being Nat holds
( P2[f . k,f . (k + 1)] & P1[f . k] )
let k be Nat; :: thesis: ( P2[f . k,f . (k + 1)] & P1[f . k] )
A13: f . k in Y by A10;
then P2[f . k,g . (f . k)] by A6;
hence ( P2[f . k,f . (k + 1)] & P1[f . k] ) by A3, A7, A13; :: thesis: verum