defpred S₁[ object , object ] means ex n being Nat st
( $2 = n & P₁[$1,n] & ( for m being Nat st P₁[$1,m] holds
n <= m ) );
A2: for x being object st x in F₁() holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in F₁() implies ex y being object st S₁[x,y] )
defpred S₂[ Nat] means P₁[x,$1];
assume x in F₁() ; :: thesis: ex y being object st S₁[x,y]
then ex n being 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]
thus S₁[x,n] by A4; :: thesis: verum

end;

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