for i, m, n being Nat st i in Seg m holds
(Sgm ((Seg (n + m)) \ (Seg n))) . i = n + i