theorem :: HILB10_2:15

for X being non empty set
for A being finite Subset of X
for R being Order of X st R linearly_orders A holds
for i, k being Nat st 1 <= i & i <= k & k <= card A holds
(SgmX (R,(rng ((SgmX (R,A)) | k)))) /. i = (SgmX (R,A)) /. i