rng p c= X ;
then reconsider g = p as Function of (dom p),X by FUNCT_2:def 1, RELSET_1:11;
A1: ( dom (f * g) = dom p & rng (f * g) c= Y & dom p = Seg (len p) ) by FINSEQ_1:def 3, FUNCT_2:def 1;
then f * g is FinSequence by FINSEQ_1:def 2;
then f * g is FinSequence of Y by A1, FINSEQ_1:def 4;
hence p * f is Element of Y * by FINSEQ_1:def 11; :: thesis: verum