theorem Th77: :: PRE_POLY:79

for X being 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 in dom (SgmX (R,B)) & (SgmX (R,B)) /. k = a holds
for i being Element of NAT st k <= i & i <= len (SgmX (R,A)) holds
(SgmX (R,B)) /. (i + 1) = (SgmX (R,A)) /. i