i < n by NAT_1:44;
hence ntoSeg is Element of Seg n by FINSEQ_3:11; :: thesis: verum