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

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;

hence F is FinSequence-yielding by PRE_POLY:def 3; :: thesis: verum