theorem :: FINSEQ_3:16

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