rng p c= I ;
then rng p c= dom f by PARTFUN1:def 4;
then dom (f * p) = dom p by RELAT_1:46
.= Seg (len p) by FINSEQ_1:def 3 ;
hence f * p is FinSequence-like by FINSEQ_1:def 2; :: thesis: verum