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 Th33;
f .: (dom f) = rng f by RELAT_1:113;
hence card (dom f) = card (rng f) by A1, Th5; :: thesis: verum