reconsider B = phi . A1 as Ordinal ;
A3: dom phi = On W by FUNCT_2:def 1;
A4: rng phi c= On W by RELAT_1:def 19;
A1 in On W by ORDINAL1:def 9;
then B in rng phi by A3, FUNCT_1:def 3;
then A5: B in On W by A4;
On W c= W by ORDINAL2:7;
hence phi . A1 is Ordinal of W by A5; :: thesis: verum