theorem Th25: :: PRE_POLY:26

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