theorem Th55: :: MESFUN11:55

for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for E being Element of S st E c= dom f & f is E -measurable holds
Integral (M,((- f) | E)) = - (Integral (M,(f | E)))