let f be Function; :: thesis: ( f is one-to-one implies card (dom f) = card (rng f) )
assume f is one-to-one ; :: thesis: card (dom f) = card (rng f)
then A1: dom f,f .: (dom f) are_equipotent by CARD_1:33;
f .: (dom f) = rng f by RELAT_1:113;
hence card (dom f) = card (rng f) by A1, CARD_1:5; :: thesis: verum