let A be set ; :: thesis: 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

let D be a_partition of A; :: thesis: for f being finite-support Function of A,REAL st f is nonpositive-yielding holds

D eqSumOf f is nonpositive-yielding

let f be finite-support Function of A,REAL; :: thesis: ( f is nonpositive-yielding implies D eqSumOf f is nonpositive-yielding )

assume f is nonpositive-yielding ; :: thesis: D eqSumOf f is nonpositive-yielding

then D eqSumOf (- f) is nonnegative-yielding ;

then - (D eqSumOf f) is nonnegative-yielding by Th54;

then - (- (D eqSumOf f)) is nonpositive-yielding ;

hence D eqSumOf f is nonpositive-yielding ; :: thesis: verum

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

D eqSumOf f is nonpositive-yielding

let D be a_partition of A; :: thesis: for f being finite-support Function of A,REAL st f is nonpositive-yielding holds

D eqSumOf f is nonpositive-yielding

let f be finite-support Function of A,REAL; :: thesis: ( f is nonpositive-yielding implies D eqSumOf f is nonpositive-yielding )

assume f is nonpositive-yielding ; :: thesis: D eqSumOf f is nonpositive-yielding

then D eqSumOf (- f) is nonnegative-yielding ;

then - (D eqSumOf f) is nonnegative-yielding by Th54;

then - (- (D eqSumOf f)) is nonpositive-yielding ;

hence D eqSumOf f is nonpositive-yielding ; :: thesis: verum