theorem Th75: :: PRE_POLY:77

for X being set
for A being finite Subset of X
for R being Order of X st R linearly_orders A holds
for i, j being Element of NAT st i in dom (SgmX (R,A)) & j in dom (SgmX (R,A)) & (SgmX (R,A)) /. i = (SgmX (R,A)) /. j holds
i = j