theorem :: CARD_2:47

for f being finite Function holds card (rng f) <= card (dom f)