let f be Function; :: thesis: ( f is Y -valued implies f is FinSequence-yielding )
assume f is Y -valued ; :: thesis: f is FinSequence-yielding
then A1: rng f c= Y ;

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 A2: x in dom f ; :: thesis: f . x is FinSequence
then reconsider D = dom f as non empty set ;
reconsider xx = x as Element of D by A2;
reconsider ff = f as Function of D,Y by FUNCT_2:2, A1;
ff . xx in Y ;
hence f . x is FinSequence ; :: thesis: verum

end;

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