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