A2: for d being Element of F₂() ex A being Ordinal st P₁[d,A]

proof

let d be Element of F₂(); :: thesis: ex A being Ordinal st P₁[d,A]
consider a being Ordinal of F₁() such that
A3: P₁[d,a] by A1;
reconsider a = a as Ordinal ;
take a ; :: thesis: P₁[d,a]
thus P₁[d,a] by A3; :: thesis: verum

end;

consider F being Function such that
A4: dom F = F₂() and
A5: 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 ) ) from ORDINAL1:sch 6(A2);
take F ; :: thesis: ( dom F = F₂() & ( for d being Element of F₂() ex a being Ordinal of F₁() st
( a = F . d & P₁[d,a] & ( for b being Ordinal of F₁() st P₁[d,b] holds
a c= b ) ) ) )
thus dom F = F₂() by A4; :: thesis: for d being Element of F₂() ex a being Ordinal of F₁() st
( a = F . d & P₁[d,a] & ( for b being Ordinal of F₁() st P₁[d,b] holds
a c= b ) )
let d be Element of F₂(); :: thesis: ex a being Ordinal of F₁() st
( a = F . d & P₁[d,a] & ( for b being Ordinal of F₁() st P₁[d,b] holds
a c= b ) )
consider A being Ordinal such that
A6: ( A = F . d & P₁[d,A] & ( for B being Ordinal st P₁[d,B] holds
A c= B ) ) by A5;
consider a being Ordinal of F₁() such that
A7: P₁[d,a] by A1;
( A c= a & a in F₁() ) by A6, A7, ORDINAL4:def 2;
then A in F₁() by CLASSES1:def 1;
then reconsider a = A as Ordinal of F₁() by ORDINAL4:def 2;
take a ; :: thesis: ( a = F . d & P₁[d,a] & ( for b being Ordinal of F₁() st P₁[d,b] holds
a c= b ) )
thus ( a = F . d & P₁[d,a] & ( for b being Ordinal of F₁() st P₁[d,b] holds
a c= b ) ) by A6; :: thesis: verum