theorem :: ORDERS_5:60

for A being Preorder
for f being finite-support Function of A,REAL
for s1 being one-to-one FinSequence of A
for s2 being one-to-one FinSequence of (QuotientOrder A) st rng s1 = support f & rng s2 = support (eqSumOf f) holds
Sum ((eqSumOf f) * s2) = Sum (f * s1)