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