theorem Th11: :: CALCUL_1:11

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