theorem :: FINSEQ_1:83

for n being Nat holds Seg n = (n + 1) \ {0}