theorem Th67: :: MESFUNC5:67

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 A, B being Element of S st f is_simple_func_in S & f is nonnegative & A misses B holds
integral' (M,(f | (A \/ B))) = (integral' (M,(f | A))) + (integral' (M,(f | B)))