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 ;
( x in Y implies ex y being object st S1[x,y] )
assume
x in Y
;
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
;
S1[x,y]
thus
S1[
x,
y]
by A3, A5;
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
; ( 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; ( 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;
( S2[k] implies S2[k + 1] )
assume
f . k in Y
;
S2[k + 1]
then
g . (f . k) in Y
by A6;
hence
S2[
k + 1]
by A7;
verum
end;
A10:
for k being Nat holds S2[k]
from NAT_1:sch 2(A8, A9);
thus
rng f c= F1()
( f . 0 = F2() & ( for k being Nat holds
( P2[f . k,f . (k + 1)] & P1[f . k] ) ) )
thus
f . 0 = F2()
by A7; for k being Nat holds
( P2[f . k,f . (k + 1)] & P1[f . k] )
let k be Nat; ( 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; verum