:: deftheorem Def16 defines eqSumOf ORDERS_5:def 16 :
for A being Preorder
for f being finite-support Function of A,REAL
for b₃ being Function of (QuotientOrder A),REAL holds
( b₃ = eqSumOf f iff for X being Element of (QuotientOrder A) st X in the carrier of (QuotientOrder A) holds
b₃ . X = Sum (f * (canFS (eqSupport (f,X)))) );