theorem :: MESFUNC6:78

for X being non empty set
for S being SigmaField of X
for f, g being PartFunc of X,REAL
for A being Element of S st A c= (dom f) /\ (dom g) & f is A -measurable & g is A -measurable holds
(max- (f + g)) + (max+ f) is A -measurable