defpred S1[ object , object ] means ( P1[$1,$2] & $2 is Ordinal of F1() );
A2:
for x being object st x in On F1() holds
ex y being object st S1[x,y]
consider f being Function such that
A4:
( dom f = On F1() & ( for x being object st x in On F1() holds
S1[x,f . x] ) )
from CLASSES1:sch 1(A2);
reconsider phi = f as Sequence by A4, ORDINAL1:def 7;
A5:
rng phi c= On F1()
then reconsider phi = phi as Ordinal-Sequence by ORDINAL2:def 4;
reconsider phi = phi as Ordinal-Sequence of F1() by A4, A5, FUNCT_2:def 1, RELSET_1:4;
take
phi
; for a being Ordinal of F1() holds P1[a,phi . a]
let a be Ordinal of F1(); P1[a,phi . a]
a in On F1()
by ORDINAL1:def 9;
hence
P1[a,phi . a]
by A4; verum