let m, n be Nat; :: thesis: ( 0 < m implies dom (Sgm ((Seg n) \/ {(n + m)})) = Seg (n + 1) )
assume 0 < m ; :: thesis: dom (Sgm ((Seg n) \/ {(n + m)})) = Seg (n + 1)
then len (Sgm ((Seg n) \/ {(n + m)})) = n + 1 by Th11;
hence dom (Sgm ((Seg n) \/ {(n + m)})) = Seg (n + 1) by FINSEQ_1:def 3; :: thesis: verum