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