theorem :: CARD_1:70
for f being Function st f is one-to-one holds
card (dom f) = card (rng f)