let f be Function; :: thesis: ( f is one-to-one implies card (dom f) = card (rng f) )
assume A1: f is one-to-one ; :: thesis: card (dom f) = card (rng f)
f .: (dom f) = rng f by RELAT_1:113;
hence card (dom f) = card (rng f) by A1, Th4, Th32; :: thesis: verum