theorem Th57: :: MESFUN11:57

for X being 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))) )