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