defpred S₁[ set , set ] means ( P₁[$1,$2] & $2 is Ordinal of F₁() );
A2: for x being set st x in On F₁() holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis: ( x in On F₁() implies ex y being set st S₁[x,y] )
assume x in On F₁() ; :: thesis: ex y being set st S₁[x,y]
then reconsider a = x as Ordinal of F₁() by ORDINAL1:def 9;
consider b being Ordinal of F₁() such that
A3: P₁[a,b] by A1;
reconsider y = b as set ;
take y ; :: thesis: S₁[x,y]
thus S₁[x,y] by A3; :: thesis: verum

end;

consider f being Function such that
A4: ( dom f = On F₁() & ( for x being set st x in On F₁() holds
S₁[x,f . x] ) ) from CLASSES1:sch 1(A2);
reconsider phi = f as T-Sequence by A4, ORDINAL1:def 7;
A5: rng phi c= On F₁()

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng phi or x in On F₁() )
assume x in rng phi ; :: thesis: x in On F₁()
then ex y being set st
( y in dom phi & x = phi . y ) by FUNCT_1:def 3;
then reconsider x = x as Ordinal of F₁() by A4;
x in F₁() ;
hence x in On F₁() 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 F₁() by A4, A5, FUNCT_2:def 1, RELSET_1:4;
take phi ; :: thesis: for a being Ordinal of F₁() holds P₁[a,phi . a]
let a be Ordinal of F₁(); :: thesis: P₁[a,phi . a]
a in On F₁() by ORDINAL1:def 9;
hence P₁[a,phi . a] by A4; :: thesis: verum