theorem :: FINSEQ_3:17

for k, n being Nat st Seg k = Seg (k + n) holds
n = 0 by Th10, FINSEQ_1:3;