let A be Preorder; :: thesis: for f being finite-support Function of A,REAL holds eqSumOf (- f) = - (eqSumOf f)
let f be finite-support Function of A,REAL; :: thesis: eqSumOf (- f) = - (eqSumOf f)
reconsider D = the carrier of (QuotientOrder A) as a_partition of the carrier of A by Th47;
thus eqSumOf (- f) = D eqSumOf (- f) by Def15
.= - (D eqSumOf f) by Th54
.= - (eqSumOf f) by Def15 ; :: thesis: verum