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