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:33;
( card (rng f) c= card (dom f) & card (rng (f ")) c= card (dom (f ")) ) by CARD_2:61;
then card (rng f) = card (dom f) by A1;
hence card f = card (rng f) by CARD_1:62; :: thesis: verum