rng p c= X ;
then reconsider g = p as Function of (dom p),X by FUNCT_2:def 1, RELSET_1:4;
A1: rng (f * g) c= Y ;
A2: dom p = Seg (len p) by FINSEQ_1:def 3;
dom (f * g) = dom p by FUNCT_2:def 1;
then f * g is FinSequence by A2, 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