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