defpred S₁[ set , set ] means ex n being Element of NAT st
( $2 = n & P₁[$1,n] & ( for m being Element of NAT st P₁[$1,m] holds
n <= m ) );
A5: for x being set st x in F₁() holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in F₁() implies ex y being set st S₁[x,y] )
defpred S₂[ Nat] means P₁[x,$1];
assume x in F₁() ; :: thesis: ex y being set st S₁[x,y]
then ex n being Element of NAT st S₂[n] by A1;
then A6: ex n being Nat st S₂[n] ;
consider n being Nat such that
A7: ( S₂[n] & ( for m being Nat st S₂[m] holds
n <= m ) ) from NAT_1:sch 5(A6);
A8: n in NAT by ORDINAL1:def 13;
take n ; :: thesis: S₁[x,n]
for m being Element of NAT st S₂[m] holds
n <= m by A7;
hence S₁[x,n] by A7, A8; :: thesis: verum

end;

thus ex f being Function st
( dom f = F₁() & ( for x being set st x in F₁() holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A5); :: thesis: verum