consider Y being set such that
A3: for x being set holds
( x in Y iff ( x in F1() & P1[x] ) ) from XBOOLE_0:sch 1();
 defpred S1[ set , set ] means ( $2 in Y & P2[$1,$2] );
A4: for x being set st x in Y holds
ex y being set st S1[x,y]
proof
let x be set ; :: thesis: ( x in Y implies ex y being set st S1[x,y] )
assume A5: x in Y ; :: thesis: ex y being set st S1[x,y]
A6: ( x in F1() & P1[x] ) by A3, A5;
consider y being set such that
A7: ( y in F1() & P2[x,y] & P1[y] ) by A2, A6;
take y ; :: thesis: S1[x,y]
thus S1[x,y] by A3, A7; :: thesis: verum
end;
consider g being Function such that
A8: ( dom g = Y & ( for x being set 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
A9: ( 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 Element of NAT holds
( P2[f . k,f . (k + 1)] & P1[f . k] ) ) )
thus dom f = NAT by A9; :: thesis: ( rng f c= F1() & f . 0 = F2() & ( for k being Element of NAT holds
( P2[f . k,f . (k + 1)] & P1[f . k] ) ) )
defpred S2[ Element of NAT ] means f . $1 in Y;
A10: S2[ 0 ] by A1, A3, A9;
A11: for k being Element of NAT st S2[k] holds
S2[k + 1]
proof
let k be Element of NAT ; :: thesis: ( S2[k] implies S2[k + 1] )
assume A12: f . k in Y ; :: thesis: S2[k + 1]
A13: g . (f . k) in Y by A8, A12;
thus S2[k + 1] by A9, A13; :: thesis: verum
end;
A14: for k being Element of NAT holds S2[k] from NAT_1:sch 1(A10, A11);
 thus rng f c= F1() :: thesis: ( f . 0 = F2() & ( for k being Element of NAT holds
( P2[f . k,f . (k + 1)] & P1[f . k] ) ) )
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng f or x in F1() )
assume A15: x in rng f ; :: thesis: x in F1()
consider y being set such that
A16: y in dom f and
A17: x = f . y by A15, FUNCT_1:def 5;
reconsider y = y as Element of NAT by A9, A16;
A18: f . y in Y by A14;
thus x in F1() by A3, A17, A18; :: thesis: verum
end;
thus f . 0 = F2() by A9; :: thesis: for k being Element of NAT holds
( P2[f . k,f . (k + 1)] & P1[f . k] )
let k be Element of NAT ; :: thesis: ( P2[f . k,f . (k + 1)] & P1[f . k] )
A19: f . k in Y by A14;
A20: P2[f . k,g . (f . k)] by A8, A19;
thus ( P2[f . k,f . (k + 1)] & P1[f . k] ) by A3, A9, A19, A20; :: thesis: verum