for n being Nat holds succ (Segm n) = Segm (n + 1)