per cases ( x in dom f or f . x = 0 ) by FUNCT_1:def 2;

suppose x in dom f ; :: thesis: f . x is Ordinal of U

then x in a by FUNCT_2:def 1;
then f . x in On U by FUNCT_2:5;
hence f . x is Ordinal of U by ORDINAL1:def 9; :: thesis: verum

end;

suppose f . x = 0 ; :: thesis: f . x is Ordinal of U

hence f . x is Ordinal of U by CLASSES2:56; :: thesis: verum

end;

end;