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

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