let f be Function; :: thesis: ( f is FinSequence-yielding iff for y being set st y in rng f holds
y is FinSequence )
hereby :: thesis: ( ( for y being set st y in rng f holds
y is FinSequence ) implies f is FinSequence-yielding )
assume A1: f is FinSequence-yielding ; :: thesis: for y being set st y in rng f holds
y is FinSequence
let y be set ; :: thesis: ( y in rng f implies y is FinSequence )
assume y in rng f ; :: thesis: y is FinSequence
then ex x being object st
( x in dom f & y = f . x ) by FUNCT_1:def 3;
hence y is FinSequence by A1; :: thesis: verum
end;
assume A2: for y being set st y in rng f holds
y is FinSequence ; :: thesis: f is FinSequence-yielding
let x be object ; :: according to PRE_POLY:def 3 :: thesis: ( x in dom f implies f . x is FinSequence )
assume x in dom f ; :: thesis: f . x is FinSequence
then f . x in rng f by FUNCT_1:def 3;
hence f . x is FinSequence by A2; :: thesis: verum