let X be non empty set ; :: thesis: for S being SigmaField of X

for M being sigma_Measure of S

for E being Element of S

for f being nonpositive PartFunc of X,ExtREAL st ex A being Element of S st

( A = dom f & f is A -measurable ) holds

( Integral (M,f) = - (integral+ (M,(max- f))) & Integral (M,f) = - (integral+ (M,(- f))) & Integral (M,f) = - (Integral (M,(- f))) )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for E being Element of S

for f being nonpositive PartFunc of X,ExtREAL st ex A being Element of S st

( A = dom f & f is A -measurable ) holds

( Integral (M,f) = - (integral+ (M,(max- f))) & Integral (M,f) = - (integral+ (M,(- f))) & Integral (M,f) = - (Integral (M,(- f))) )

let M be sigma_Measure of S; :: thesis: for E being Element of S

for f being nonpositive PartFunc of X,ExtREAL st ex A being Element of S st

( A = dom f & f is A -measurable ) holds

( Integral (M,f) = - (integral+ (M,(max- f))) & Integral (M,f) = - (integral+ (M,(- f))) & Integral (M,f) = - (Integral (M,(- f))) )

let E be Element of S; :: thesis: for f being nonpositive PartFunc of X,ExtREAL st ex A being Element of S st

( A = dom f & f is A -measurable ) holds

( Integral (M,f) = - (integral+ (M,(max- f))) & Integral (M,f) = - (integral+ (M,(- f))) & Integral (M,f) = - (Integral (M,(- f))) )

let f be nonpositive PartFunc of X,ExtREAL; :: thesis: ( ex A being Element of S st

( A = dom f & f is A -measurable ) implies ( Integral (M,f) = - (integral+ (M,(max- f))) & Integral (M,f) = - (integral+ (M,(- f))) & Integral (M,f) = - (Integral (M,(- f))) ) )

assume ex A being Element of S st

( A = dom f & f is A -measurable ) ; :: thesis: ( Integral (M,f) = - (integral+ (M,(max- f))) & Integral (M,f) = - (integral+ (M,(- f))) & Integral (M,f) = - (Integral (M,(- f))) )

then consider A being Element of S such that

A2: ( A = dom f & f is A -measurable ) ;

A3: dom (max+ f) = A by A2, MESFUNC2:def 2;

A4: f = - (max- f) by Th32;

then A5: - f = max- f by Th36;

for x being Element of X st x in dom (max+ f) holds

(max+ f) . x = 0

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

.= (integral+ (M,(max+ f))) + (- (integral+ (M,(max- f)))) by XXREAL_3:def 4 ;

hence Integral (M,f) = - (integral+ (M,(max- f))) by A6, XXREAL_3:4; :: thesis: ( Integral (M,f) = - (integral+ (M,(- f))) & Integral (M,f) = - (Integral (M,(- f))) )

thus A8: Integral (M,f) = - (integral+ (M,(- f))) by A5, A7, A6, XXREAL_3:4; :: thesis: Integral (M,f) = - (Integral (M,(- f)))

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

hence Integral (M,f) = - (Integral (M,(- f))) by A8, A2, MEASUR11:63, MESFUNC5:88; :: thesis: verum

for M being sigma_Measure of S

for E being Element of S

for f being nonpositive PartFunc of X,ExtREAL st ex A being Element of S st

( A = dom f & f is A -measurable ) holds

( Integral (M,f) = - (integral+ (M,(max- f))) & Integral (M,f) = - (integral+ (M,(- f))) & Integral (M,f) = - (Integral (M,(- f))) )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for E being Element of S

for f being nonpositive PartFunc of X,ExtREAL st ex A being Element of S st

( A = dom f & f is A -measurable ) holds

( Integral (M,f) = - (integral+ (M,(max- f))) & Integral (M,f) = - (integral+ (M,(- f))) & Integral (M,f) = - (Integral (M,(- f))) )

let M be sigma_Measure of S; :: thesis: for E being Element of S

for f being nonpositive PartFunc of X,ExtREAL st ex A being Element of S st

( A = dom f & f is A -measurable ) holds

( Integral (M,f) = - (integral+ (M,(max- f))) & Integral (M,f) = - (integral+ (M,(- f))) & Integral (M,f) = - (Integral (M,(- f))) )

let E be Element of S; :: thesis: for f being nonpositive PartFunc of X,ExtREAL st ex A being Element of S st

( A = dom f & f is A -measurable ) holds

( Integral (M,f) = - (integral+ (M,(max- f))) & Integral (M,f) = - (integral+ (M,(- f))) & Integral (M,f) = - (Integral (M,(- f))) )

let f be nonpositive PartFunc of X,ExtREAL; :: thesis: ( ex A being Element of S st

( A = dom f & f is A -measurable ) implies ( Integral (M,f) = - (integral+ (M,(max- f))) & Integral (M,f) = - (integral+ (M,(- f))) & Integral (M,f) = - (Integral (M,(- f))) ) )

assume ex A being Element of S st

( A = dom f & f is A -measurable ) ; :: thesis: ( Integral (M,f) = - (integral+ (M,(max- f))) & Integral (M,f) = - (integral+ (M,(- f))) & Integral (M,f) = - (Integral (M,(- f))) )

then consider A being Element of S such that

A2: ( A = dom f & f is A -measurable ) ;

A3: dom (max+ f) = A by A2, MESFUNC2:def 2;

A4: f = - (max- f) by Th32;

then A5: - f = max- f by Th36;

for x being Element of X st x in dom (max+ f) holds

(max+ f) . x = 0

proof

then A6:
integral+ (M,(max+ f)) = 0
by A3, A2, MESFUNC2:25, MESFUNC5:87;
let x be Element of X; :: thesis: ( x in dom (max+ f) implies (max+ f) . x = 0 )

assume x in dom (max+ f) ; :: thesis: (max+ f) . x = 0

then f . x = - ((max- f) . x) by A2, A3, A4, MESFUNC1:def 7;

then - (f . x) = (max- f) . x ;

hence (max+ f) . x = 0 by MESFUNC2:21; :: thesis: verum

end;assume x in dom (max+ f) ; :: thesis: (max+ f) . x = 0

then f . x = - ((max- f) . x) by A2, A3, A4, MESFUNC1:def 7;

then - (f . x) = (max- f) . x ;

hence (max+ f) . x = 0 by MESFUNC2:21; :: thesis: verum

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

.= (integral+ (M,(max+ f))) + (- (integral+ (M,(max- f)))) by XXREAL_3:def 4 ;

hence Integral (M,f) = - (integral+ (M,(max- f))) by A6, XXREAL_3:4; :: thesis: ( Integral (M,f) = - (integral+ (M,(- f))) & Integral (M,f) = - (Integral (M,(- f))) )

thus A8: Integral (M,f) = - (integral+ (M,(- f))) by A5, A7, A6, XXREAL_3:4; :: thesis: Integral (M,f) = - (Integral (M,(- f)))

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

hence Integral (M,f) = - (Integral (M,(- f))) by A8, A2, MEASUR11:63, MESFUNC5:88; :: thesis: verum