theorem Th6: :: MESFUNC2:6

for X being non empty set
for r being Real
for S being SigmaField of X
for f, g being PartFunc of X,ExtREAL
for A being Element of S st f is A -measurable & g is A -measurable holds
ex F being Function of RAT,S st
for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p))))