take f = N --> {{}}; :: thesis: f is N -element
card (dom f) = N ;
hence card f = N by Th60; :: according to CARD_1:def 7 :: thesis: verum