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