per cases ;

suppose F₁() = {} ; :: thesis:

then A2: for e being object st e in F₁() holds
ex u being object st
( u in {} & P₁[e,u] ) ;
ex f being Function st
( dom f = F₁() & rng f c= {} & ( for e being object st e in F₁() holds
P₁[e,f . e] ) ) from FUNCT_1:sch 6(A2);
hence ex f being Function st
( dom f = F₁() & ( for e being object st e in F₁() holds
P₁[e,f . e] ) ) ; :: thesis:

end;

suppose F₁() <> {} ; :: thesis:

then reconsider D = F₁() as non empty set ;
defpred S₁[ set , Ordinal] means ex u being set st
( u in Rank $2 & P₁[$1,u] );
A3: for e being Element of D ex A being Ordinal st S₁[e,A]

proof

let e be Element of D; :: thesis:
consider u being object such that
A4: P₁[e,u] by A1;
reconsider u = u as set by TARSKI:1;
u c= Rank (the_rank_of u) by Def9;
then u in Rank (succ (the_rank_of u)) by Th32;
hence ex A being Ordinal st S₁[e,A] by A4; :: thesis:

end;

consider F being Function such that
A5: ( dom F = D & ( for d being Element of D ex A being Ordinal st
( A = F . d & S₁[d,A] & ( for B being Ordinal st S₁[d,B] holds
A c= B ) ) ) ) from ORDINAL1:sch 6(A3);
A6: for e being object st e in F₁() holds
ex u being object st
( u in Rank (sup (rng F)) & P₁[e,u] )

proof

let e be object ; :: thesis:
assume A7: e in F₁() ; :: thesis:
then consider A being Ordinal such that
A8: A = F . e and
A9: ex u being set st
( u in Rank A & P₁[e,u] ) and
for B being Ordinal st ex u being set st
( u in Rank B & P₁[e,u] ) holds
A c= B by A5;
consider u being set such that
A10: ( u in Rank A & P₁[e,u] ) by A9;
take u ; :: thesis:
A in rng F by A5, A7, A8, FUNCT_1:def 3;
then A in sup (rng F) by ORDINAL2:19;
then Rank A c= Rank (sup (rng F)) by Th37, ORDINAL1:def 2;
hence ( u in Rank (sup (rng F)) & P₁[e,u] ) by A10; :: thesis:

end;

ex f being Function st
( dom f = F₁() & rng f c= Rank (sup (rng F)) & ( for e being object st e in F₁() holds
P₁[e,f . e] ) ) from FUNCT_1:sch 6(A6);
hence ex f being Function st
( dom f = F₁() & ( for e being object st e in F₁() holds
P₁[e,f . e] ) ) ; :: thesis:

end;

end;