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;