let X be non empty set ; :: thesis: 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_measurable_on A & g is_measurable_on A 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))))
let S be SigmaField of X; :: thesis: for f, g being PartFunc of X,REAL
for A being Element of S
for r being Real st f is_measurable_on A & g is_measurable_on A 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))))
let f, g be PartFunc of X,REAL; :: thesis: for A being Element of S
for r being Real st f is_measurable_on A & g is_measurable_on A 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))))
let A be Element of S; :: thesis: for r being Real st f is_measurable_on A & g is_measurable_on A 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))))
let r be Real; :: thesis: ( f is_measurable_on A & g is_measurable_on A implies 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)))) )
assume ( f is_measurable_on A & g is_measurable_on A ) ; :: thesis: 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))))
then ( R_EAL f is_measurable_on A & R_EAL g is_measurable_on A ) by Def6;
then consider F being Function of RAT,S such that
A1: for p being Rational holds F . p = (A /\ (less_dom ((R_EAL f),(R_EAL p)))) /\ (A /\ (less_dom ((R_EAL g),(R_EAL (r - p))))) by MESFUNC2:6;

now

let p be Rational; :: thesis: F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p))))
thus F . p = (A /\ (less_dom ((R_EAL f),(R_EAL p)))) /\ (A /\ (less_dom ((R_EAL g),(R_EAL (r - p))))) by A1
.= (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ; :: thesis: verum

end;

hence 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)))) ; :: thesis: verum