for A being set
for D being a_partition of A
for f being finite-support Function of A,REAL st f is nonpositive-yielding holds
D eqSumOf f is nonpositive-yielding