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 A1, MESFUNC2:def 2, MESFUNC2:def 3;

B7: ( max- f is A -measurable & max+ f is A -measurable ) by A1, A2, Th10;

A6: dom (- f) = A by A1, MESFUNC1:def 7;

then A7: ( dom (max+ (- f)) = A & dom (max- (- f)) = A ) by MESFUNC2:def 2, MESFUNC2:def 3;

- f is A -measurable by A1, A2, MEASUR11:63;

then A9: ( max+ (- f) is A -measurable & max- (- f) is A -measurable ) by A6, Th10;

then P1: integral+ (M,(max+ (- f))) = Integral (M,(max+ (- f))) by A7, Th5, MESFUNC5:88

.= Integral (M,(max- (- (- f)))) by Th34

.= integral+ (M,(max- f)) by A4, B6, B7, Th5, MESFUNC5:88 ;

integral+ (M,(max- (- f))) = Integral (M,(max- (- f))) by A7, A9, Th5, MESFUNC5:88

.= Integral (M,(max+ (- (- f)))) by MESFUNC2:14

.= integral+ (M,(max+ f)) by A4, B6, B7, Th5, MESFUNC5:88 ;

then Integral (M,f) = (integral+ (M,(max- (- f)))) - (integral+ (M,(max+ (- f)))) by P1, MESFUNC5:def 16

.= - ((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

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 A1, MESFUNC2:def 2, MESFUNC2:def 3;

B7: ( max- f is A -measurable & max+ f is A -measurable ) by A1, A2, Th10;

A6: dom (- f) = A by A1, MESFUNC1:def 7;

then A7: ( dom (max+ (- f)) = A & dom (max- (- f)) = A ) by MESFUNC2:def 2, MESFUNC2:def 3;

- f is A -measurable by A1, A2, MEASUR11:63;

then A9: ( max+ (- f) is A -measurable & max- (- f) is A -measurable ) by A6, Th10;

then P1: integral+ (M,(max+ (- f))) = Integral (M,(max+ (- f))) by A7, Th5, MESFUNC5:88

.= Integral (M,(max- (- (- f)))) by Th34

.= integral+ (M,(max- f)) by A4, B6, B7, Th5, MESFUNC5:88 ;

integral+ (M,(max- (- f))) = Integral (M,(max- (- f))) by A7, A9, Th5, MESFUNC5:88

.= Integral (M,(max+ (- (- f)))) by MESFUNC2:14

.= integral+ (M,(max+ f)) by A4, B6, B7, Th5, MESFUNC5:88 ;

then Integral (M,f) = (integral+ (M,(max- (- f)))) - (integral+ (M,(max+ (- f)))) by P1, MESFUNC5:def 16

.= - ((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