theorem Th16: :: HILB10_2:16

for n, m being Nat
for O being Ordinal
for A being finite Subset of (Bags O) st n in dom (SgmX ((BagOrder O),A)) & m in dom (SgmX ((BagOrder O),A)) & n < m holds
(SgmX ((BagOrder O),A)) /. n < (SgmX ((BagOrder O),A)) /. m