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