for k being Nat holds Seg k <> Seg (k + 1) by Th8, FINSEQ_1:4;