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