let F be Function of (TOP-REAL n),(TOP-REAL m); :: 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 ( rng F c= the carrier of (TOP-REAL m) & F . x in rng F ) by FUNCT_1:def 3, RELAT_1:def 19;
hence F . x is FinSequence ; :: thesis: verum

end;

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