for m, n being Nat st 0 < m holds
len (Sgm ((Seg n) \/ {(n + m)})) = n + 1