card f = N by Def6;
hence card (dom f) = N by Th60; :: according to CARD_1:def 7 :: thesis: verum