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