A1: dom (f | X) c= dom f by RELAT_1:60;

now :: thesis: for x being object st x in dom (f | X) holds
(f | X) . x is FinSequence

let x be object ; :: thesis: ( x in dom (f | X) implies (f | X) . x is FinSequence )
assume x in dom (f | X) ; :: thesis: (f | X) . x is FinSequence
then ( x in dom f & (f | X) . x = f . x ) by FUNCT_1:47, A1;
hence (f | X) . x is FinSequence ; :: thesis: verum

end;

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