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 set st
( x in dom f & y = f . x ) by FUNCT_1:def 5;
hence y is FinSequence by A1, MATRLIN:def 1; :: 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 set ; :: according to MATRLIN:def 1 :: thesis: ( not x in dom f or f . x is set )
assume x in dom f ; :: thesis: f . x is set
then f . x in rng f by FUNCT_1:def 5;
hence f . x is set by A2; :: thesis: verum