theorem Th21: :: PRE_POLY:22

for f being Function holds
( f is Cardinal-yielding iff for y being set st y in rng f holds
y is Cardinal )