theorem :: CARD_2:61

for f being Function holds card (rng f) c= card (dom f)