not 0 in Seg n by FINSEQ_1:1;
hence Seg n is without_zero by MEASURE6:def 2; :: thesis: verum