let q be Seg (m + m0) -defined Relation; :: thesis: ( q = p null m0 implies q is total )
assume q = p null m0 ; :: thesis: q is total
then dom q = Seg (m + m0) by FINSEQ_1:89;
hence q is total by PARTFUN1:def 2; :: thesis: verum