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