succ (Segm i) = Segm (i + 1) by NAT_1:38;
hence ntoSeg is Element of Seg n by FINSEQ_3:11, NAT_1:44; :: thesis: verum