reconsider mm = m as Element of NAT by ORDINAL1:def 12;
set q = p | (Seg m);
set N = m + n;
( m + 0 <= m + n & len p = m + n ) by XREAL_1:7, CARD_1:def 7;
then ( Seg m c= Seg (m + n) & dom p = Seg (m + n) ) by FINSEQ_1:5, FINSEQ_1:def 3;
then reconsider M = Seg m as Subset of (dom p) ;
dom (p | (Seg m)) = M null (dom p) by RELAT_1:61
.= Seg mm ;
then len (p | (Seg m)) = mm by FINSEQ_1:def 3;
hence for b₁ being FinSequence st b₁ = p | (Seg m) holds
b₁ is m -element by CARD_1:def 7; :: thesis: verum