:: deftheorem Def15 defines eqSumOf ORDERS_5:def 15 :
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 ex D being a_partition of the carrier of A st
( D = the carrier of (QuotientOrder A) & b₃ = D eqSumOf f ) );