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

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:7;
hence f . x is Ordinal of U by ORDINAL1:def 10; :: thesis: verum

end;

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

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

end;

end;