let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for A being Element of S st A = dom f & f is A -measurable holds
Integral (M,(- f)) = - (Integral (M,f))

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for A being Element of S st A = dom f & f is A -measurable holds
Integral (M,(- f)) = - (Integral (M,f))

let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL
for A being Element of S st A = dom f & f is A -measurable holds
Integral (M,(- f)) = - (Integral (M,f))

let f be PartFunc of X,ExtREAL; :: thesis: for A being Element of S st A = dom f & f is A -measurable holds
Integral (M,(- f)) = - (Integral (M,f))

let A be Element of S; :: thesis: ( A = dom f & f is A -measurable implies Integral (M,(- f)) = - (Integral (M,f)) )
assume that
A1: A = dom f and
A2: f is A -measurable ; :: thesis: Integral (M,(- f)) = - (Integral (M,f))
set g = - f;
A4: f = - (- f) by Th36;
B6: ( dom (max- f) = A & dom (max+ f) = A ) by ;
B7: ( max- f is A -measurable & max+ f is A -measurable ) by A1, A2, Th10;
A6: dom (- f) = A by ;
then A7: ( dom (max+ (- f)) = A & dom (max- (- f)) = A ) by ;
- f is A -measurable by ;
then A9: ( max+ (- f) is A -measurable & max- (- f) is A -measurable ) by ;
then P1: integral+ (M,(max+ (- f))) = Integral (M,(max+ (- f))) by
.= Integral (M,(max- (- (- f)))) by Th34
.= integral+ (M,(max- f)) by ;
integral+ (M,(max- (- f))) = Integral (M,(max- (- f))) by
.= Integral (M,(max+ (- (- f)))) by MESFUNC2:14
.= integral+ (M,(max+ f)) by ;
then Integral (M,f) = (integral+ (M,(max- (- f)))) - (integral+ (M,(max+ (- f)))) by
.= - ((integral+ (M,(max+ (- f)))) - (integral+ (M,(max- (- f))))) by XXREAL_3:26 ;
hence Integral (M,(- f)) = - (Integral (M,f)) by MESFUNC5:def 16; :: thesis: verum