theorem :: MESFUN12:23

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