reconsider mm = m as Element of NAT by ORDINAL1:def 13;
( rng p c= X & dom f = X ) by RELAT_1:def 19, FUNCT_2:def 1;
then dom (f * p) = dom p by RELAT_1:46
.= Seg (len p) by FINSEQ_1:def 3
.= Seg mm by CARD_1:def 13 ;
then len (f * p) = mm by FINSEQ_1:def 3;
hence f * p is m -element by CARD_1:def 13; :: thesis: verum