theorem Th18: :: PRE_POLY:19

for f being one-to-one Function holds card f = card (rng f)