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]
proof
let x be object ; :: thesis: ( x in On F1() implies ex y being object st S1[x,y] )
assume x in On F1() ; :: thesis: ex y being object st S1[x,y]
then reconsider a = x as Ordinal of F1() by ORDINAL1:def 9;
consider b being Ordinal of F1() such that
A3: P1[a,b] by A1;
reconsider y = b as set ;
take y ; :: thesis: S1[x,y]
thus S1[x,y] by A3; :: thesis: verum
end;
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()
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng phi or x in On F1() )
assume x in rng phi ; :: thesis: x in On F1()
then ex y being object st
( y in dom phi & x = phi . y ) by FUNCT_1:def 3;
then reconsider x = x as Ordinal of F1() by A4;
x in F1() ;
hence x in On F1() by ORDINAL1:def 9; :: thesis: verum
end;
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 ; :: thesis: for a being Ordinal of F1() holds P1[a,phi . a]
let a be Ordinal of F1(); :: thesis: P1[a,phi . a]
a in On F1() by ORDINAL1:def 9;
hence P1[a,phi . a] by A4; :: thesis: verum