:: deftheorem Def14 defines eqSumOf ORDERS_5:def 14 :
for A being set
for D being a_partition of A
for f being finite-support Function of A,REAL
for b₄ being Function of D,REAL holds
( b₄ = D eqSumOf f iff for X being Element of D st X in D holds
b₄ . X = Sum (f * (canFS (eqSupport (f,X)))) );