reconsider l = len p as Element of NAT ;
dom p = Seg l by FINSEQ_1:def 3
.= Seg m by CARD_1:def 7 ;
hence for b₁ being Seg (m + m0) -defined Relation st b₁ = p null m0 holds
b₁ is total by PARTFUN1:def 2; :: thesis: verum