let f be finite Function; :: thesis: card (rng f) <= card (dom f)
reconsider X = rng f, Y = dom f as set ;
card X c= card Y by CARD_1:12;
hence card (rng f) <= card (dom f) by NAT_1:39; :: thesis: verum