let f be one-to-one Function; :: thesis: card f = card (rng f)
A1: ( rng f = dom (f " ) & dom f = rng (f " ) ) by FUNCT_1:55;
( card (rng f) c= card (dom f) & card (rng (f " )) c= card (dom (f " )) ) by CARD_2:80;
then card (rng f) = card (dom f) by A1, XBOOLE_0:def 10;
hence card f = card (rng f) by CARD_1:104; :: thesis: verum