let f be Function; :: thesis: ( f is Cardinal-yielding implies f is Ordinal-yielding )
assume f is Cardinal-yielding ; :: thesis: f is Ordinal-yielding
then for x being object st x in dom f holds
f . x is Ordinal by CARD_3:def 1;
hence f is Ordinal-yielding by Th2; :: thesis: verum