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