for X being non empty set
for A being finite Subset of X
for a being Element of X st not a in A holds
for B being finite Subset of X st B = {a} \/ A holds
for R being Order of X st R linearly_orders B holds
for k being Element of NAT st k + 1 in dom (SgmX (R,B)) & (SgmX (R,B)) /. (k + 1) = a holds
SgmX (R,B) = Ins ((SgmX (R,A)),k,a)