let f be finite Function; :: thesis: card (rng f) <= card (dom f)
Segm (card (rng f)) c= Segm (card (dom f)) by CARD_1:12;
hence card (rng f) <= card (dom f) by NAT_1:39; :: thesis: verum