let f be Function; :: thesis: ( f is empty implies f is Cardinal-yielding )
assume A1: f is empty ; :: thesis: f is Cardinal-yielding
let x be set ; :: according to CARD_3:def 1 :: thesis: ( x in dom f implies f . x is Cardinal )
thus ( x in dom f implies f . x is Cardinal ) by A1; :: thesis: verum