rng p c= X ;
then reconsider pp = p as FinSequence of X by FINSEQ_1:def 4;
f * pp is FinSequence of Y ;
hence f * p is FinSequence-like ; :: thesis: verum