per cases ( F₁() = {} or F₁() <> {} ) ;

suppose F₁() = {} ; :: thesis: ex f being Function st
( dom f = F₁() & ( for e being set st e in F₁() holds
P₁[e,f . e] ) )

then A3: for e being set st e in F₁() holds
ex u being set st
( u in {} & P₁[e,u] ) ;
ex f being Function st
( dom f = F₁() & rng f c= {} & ( for e being set st e in F₁() holds
P₁[e,f . e] ) ) from WELLORD2:sch 1(A3);
hence ex f being Function st
( dom f = F₁() & ( for e being set st e in F₁() holds
P₁[e,f . e] ) ) ; :: thesis: verum

end;

suppose F₁() <> {} ; :: thesis: ex f being Function st
( dom f = F₁() & ( for e being set st e in F₁() holds
P₁[e,f . e] ) )

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] );
A6: for e being Element of D ex A being Ordinal st S₁[e,A]

proof

let e be Element of D; :: thesis: ex A being Ordinal st S₁[e,A]
consider u being set such that
A7: P₁[e,u] by A1;
u c= Rank (the_rank_of u) by Def8;
then u in Rank (succ (the_rank_of u)) by Th36;
hence ex A being Ordinal st S₁[e,A] by A7; :: thesis: verum

end;

consider F being Function such that
A10: ( 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(A6);
A11: for e being set st e in F₁() holds
ex u being set st
( u in Rank (sup (rng F)) & P₁[e,u] )

proof

let e be set ; :: thesis: ( e in F₁() implies ex u being set st
( u in Rank (sup (rng F)) & P₁[e,u] ) )
assume A12: e in F₁() ; :: thesis: ex u being set st
( u in Rank (sup (rng F)) & P₁[e,u] )
then consider A being Ordinal such that
A13: A = F . e and
A14: 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 A10;
consider u being set such that
A15: ( u in Rank A & P₁[e,u] ) by A14;
take u ; :: thesis: ( u in Rank (sup (rng F)) & P₁[e,u] )
A in rng F by A10, A12, A13, FUNCT_1:def 5;
then A in sup (rng F) by ORDINAL2:27;
then A c= sup (rng F) by ORDINAL1:def 2;
then Rank A c= Rank (sup (rng F)) by Th43;
hence ( u in Rank (sup (rng F)) & P₁[e,u] ) by A15; :: thesis: verum

end;

ex f being Function st
( dom f = F₁() & rng f c= Rank (sup (rng F)) & ( for e being set st e in F₁() holds
P₁[e,f . e] ) ) from WELLORD2:sch 1(A11);
hence ex f being Function st
( dom f = F₁() & ( for e being set st e in F₁() holds
P₁[e,f . e] ) ) ; :: thesis: verum

end;

end;