let X be non empty set ; 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; 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; 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; 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; ( 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 )
; ( 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
then A6:
integral+ (M,(max+ f)) = 0
by A3, A2, MESFUNC2:25, MESFUNC5:87;
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; ( 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; 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; verum