A1: ( A1 in On W & dom phi = On W ) by FUNCT_2:def 1, ORDINAL1:def 10;
reconsider B = phi . A1 as Ordinal ;
( B in rng phi & rng phi c= On W ) by A1, FUNCT_1:def 5, RELAT_1:def 19;
then ( B in On W & On W c= W ) by ORDINAL2:9;
hence phi . A1 is Ordinal of W ; :: thesis: verum