theorem Th10: :: FINSEQ_3:10

for k, n being Nat st k + n in Seg k holds
n = 0