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