theorem Th2: :: COUNTERS:32

for f being Function holds
( f is Ordinal-yielding iff for x being object st x in dom f holds
f . x is Ordinal )