defpred S₁[ object , object ] means ex A being Ordinal st
( A = $2 & P₁[$1,A] & ( for B being Ordinal st P₁[$1,B] holds
A c= B ) );
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] )
assume x in F₁() ; :: thesis: ex y being object st S₁[x,y]
then reconsider d = x as Element of F₁() ;
defpred S₂[ Ordinal] means P₁[d,$1];
A3: ex A being Ordinal st S₂[A] by A1;
consider A being Ordinal such that
A4: ( S₂[A] & ( for B being Ordinal st S₂[B] holds
A c= B ) ) from ORDINAL1:sch 1(A3);
reconsider y = A as set ;
take y ; :: thesis: S₁[x,y]
take A ; :: thesis: ( A = y & P₁[x,A] & ( for B being Ordinal st P₁[x,B] holds
A c= B ) )
thus ( A = y & P₁[x,A] & ( for B being Ordinal st P₁[x,B] holds
A c= B ) ) by A4; :: thesis: verum

end;

A5: for x, y, z being object st x in F₁() & S₁[x,y] & S₁[x,z] holds
y = z

proof

let x, y, z be object ; :: thesis: ( x in F₁() & S₁[x,y] & S₁[x,z] implies y = z )
assume x in F₁() ; :: thesis: ( not S₁[x,y] or not S₁[x,z] or y = z )
given A1 being Ordinal such that A6: A1 = y and
A7: ( P₁[x,A1] & ( for B being Ordinal st P₁[x,B] holds
A1 c= B ) ) ; :: thesis: ( not S₁[x,z] or y = z )
given A2 being Ordinal such that A8: A2 = z and
A9: ( P₁[x,A2] & ( for B being Ordinal st P₁[x,B] holds
A2 c= B ) ) ; :: thesis: y = z
( A1 c= A2 & A2 c= A1 ) by A7, A9;
hence y = z by A6, A8, XBOOLE_0:def 10; :: thesis: verum

end;

consider F being Function such that
A10: ( dom F = F₁() & ( for x being object st x in F₁() holds
S₁[x,F . x] ) ) from FUNCT_1:sch 2(A5, A2);
take F ; :: thesis: ( dom F = F₁() & ( for d being Element of F₁() ex A being Ordinal st
( A = F . d & P₁[d,A] & ( for B being Ordinal st P₁[d,B] holds
A c= B ) ) ) )
thus dom F = F₁() by A10; :: thesis: for d being Element of F₁() ex A being Ordinal st
( A = F . d & P₁[d,A] & ( for B being Ordinal st P₁[d,B] holds
A c= B ) )
let d be Element of F₁(); :: thesis: ex A being Ordinal st
( A = F . d & P₁[d,A] & ( for B being Ordinal st P₁[d,B] holds
A c= B ) )
thus ex A being Ordinal st
( A = F . d & P₁[d,A] & ( for B being Ordinal st P₁[d,B] holds
A c= B ) ) by A10; :: thesis: verum