theorem :: MESFUNC6:25

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
for r being Real 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)))) by MESFUNC2:6;