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

eqSumOf f is nonpositive-yielding

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

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

reconsider D = the carrier of (QuotientOrder A) as a_partition of the carrier of A by Th47;

D eqSumOf f is nonpositive-yielding by A1, Th58;

hence eqSumOf f is nonpositive-yielding by Def15; :: thesis: verum

eqSumOf f is nonpositive-yielding

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

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

reconsider D = the carrier of (QuotientOrder A) as a_partition of the carrier of A by Th47;

D eqSumOf f is nonpositive-yielding by A1, Th58;

hence eqSumOf f is nonpositive-yielding by Def15; :: thesis: verum