theorem Th21: :: MESFUN12:21

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 nonnegative & g is E2 -measurable holds
Integral (M,(f + g)) = (Integral (M,(f | (dom (f + g))))) + (Integral (M,(g | (dom (f + g)))))