reconsider mm = m as Element of NAT by ORDINAL1:def 12;
( rng p c= X & dom f = X ) by FUNCT_2:def 1;
then dom (f * p) = dom p by RELAT_1:27
.= Seg (len p) by FINSEQ_1:def 3
.= Seg mm by CARD_1:def 7 ;
then len (f * p) = mm by FINSEQ_1:def 3;
hence for b₁ being set st b₁ = f * p holds
b₁ is m -element by CARD_1:def 7; :: thesis: verum