dom p = Seg (len p) by FINSEQ_1:def 3;
then ( m + 0 <= m + n & dom p = Seg m ) by CARD_1:def 7, XREAL_1:6;
hence for b₁ being Relation st b₁ = p null n holds
b₁ is Seg (m + n) -defined by FINSEQ_1:5; :: thesis: verum