theorem :: FINSEQ_1:4

for a being natural Number holds a + 1 in Seg (a + 1) by Th3;