theorem Th12: :: CALCUL_1:12

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