theorem Th58: :: MESFUN11:58

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being nonpositive PartFunc of X,ExtREAL st f is_simple_func_in S holds
( Integral (M,f) = - (integral' (M,(- f))) & Integral (M,f) = - (integral' (M,(max- f))) )