let F be Function of X,(TOP-REAL n); :: thesis: F is FinSequence-yielding

now :: thesis: for x being object st x in dom F holds

F . x is FinSequence

hence
F is FinSequence-yielding
by PRE_POLY:def 3; :: thesis: verumF . x is FinSequence

let x be object ; :: 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 ; :: thesis: verum

end;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 ; :: thesis: verum