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

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

A3: for e being set st e in F₁() holds
ex u being set st
( u in {} & P₁[e,u] ) by A2;
A4: 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);
thus ex f being Function st
( dom f = F₁() & ( for e being set st e in F₁() holds
P₁[e,f . e] ) ) by A4; :: thesis: verum

end;

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

reconsider D = F₁() as non empty set by A5;
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;
A8: u c= Rank (the_rank_of u) by Def8;
A9: u in Rank (succ (the_rank_of u)) by A8, Th36;
thus ex A being Ordinal st S₁[e,A] by A7, A9; :: 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] )
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, A12;
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] )
A16: A in rng F by A10, A12, A13, FUNCT_1:def 5;
A17: A in sup (rng F) by A16, ORDINAL2:27;
A18: A c= sup (rng F) by A17, ORDINAL1:def 2;
A19: Rank A c= Rank (sup (rng F)) by A18, Th43;
thus ( u in Rank (sup (rng F)) & P₁[e,u] ) by A15, A19; :: thesis: verum

end;

A20: 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);
thus ex f being Function st
( dom f = F₁() & ( for e being set st e in F₁() holds
P₁[e,f . e] ) ) by A20; :: thesis: verum

end;

end;