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 ) );
A2: 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 A3: ex n being Nat st S₂[n] ;
consider n being Nat such that
A4: ( S₂[n] & ( for m being Nat st S₂[m] holds
n <= m ) ) from NAT_1:sch 5(A3);
take n ; :: thesis: S₁[x,n]
( n in NAT & ( for m being Element of NAT st S₂[m] holds
n <= m ) ) by A4, ORDINAL1:def 12;
hence S₁[x,n] by A4; :: 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(A2); :: thesis: verum