let f be Function; :: thesis: card (rng f) c= card (dom f)
rng f = f .: (dom f) by RELAT_1:113;
hence card (rng f) c= card (dom f) by CARD_1:66; :: thesis: verum