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

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