theorem Th47: :: MESFUNC5:47

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