let X be non empty set ; :: thesis: 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_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,(R_EAL p))) /\ (A /\ (less_dom g,(R_EAL (r - p))))
let r be Real; :: thesis: for S being SigmaField of X
for f, g being PartFunc of X,ExtREAL
for A being Element of S 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,(R_EAL p))) /\ (A /\ (less_dom g,(R_EAL (r - p))))
let S be SigmaField of X; :: thesis: for f, g being PartFunc of X,ExtREAL
for A being Element of S 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,(R_EAL p))) /\ (A /\ (less_dom g,(R_EAL (r - p))))
let f, g be PartFunc of X,ExtREAL ; :: thesis: for A being Element of S 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,(R_EAL p))) /\ (A /\ (less_dom g,(R_EAL (r - p))))
let A be Element of S; :: 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,(R_EAL p))) /\ (A /\ (less_dom g,(R_EAL (r - p)))) )
assume A1: ( 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,(R_EAL p))) /\ (A /\ (less_dom g,(R_EAL (r - p))))
defpred S₁[ set , set ] means ex p being Rational st
( p = $1 & $2 = (A /\ (less_dom f,(R_EAL p))) /\ (A /\ (less_dom g,(R_EAL (r - p)))) );
A2: for x1 being set st x1 in RAT holds
ex y1 being set st
( y1 in S & S₁[x1,y1] )

proof

let x1 be set ; :: thesis: ( x1 in RAT implies ex y1 being set st
( y1 in S & S₁[x1,y1] ) )
assume A3: x1 in RAT ; :: thesis: ex y1 being set st
( y1 in S & S₁[x1,y1] )
consider p being Rational such that
A4: p = x1 by A3;
A5: ( A /\ (less_dom f,(R_EAL p)) in S & A /\ (less_dom g,(R_EAL (r - p))) in S ) by A1, MESFUNC1:def 17;
take (A /\ (less_dom f,(R_EAL p))) /\ (A /\ (less_dom g,(R_EAL (r - p)))) ; :: thesis: ( (A /\ (less_dom f,(R_EAL p))) /\ (A /\ (less_dom g,(R_EAL (r - p)))) in S & S₁[x1,(A /\ (less_dom f,(R_EAL p))) /\ (A /\ (less_dom g,(R_EAL (r - p))))] )
thus ( (A /\ (less_dom f,(R_EAL p))) /\ (A /\ (less_dom g,(R_EAL (r - p)))) in S & S₁[x1,(A /\ (less_dom f,(R_EAL p))) /\ (A /\ (less_dom g,(R_EAL (r - p))))] ) by A4, A5, FINSUB_1:def 2; :: thesis: verum

end;

consider G being Function of RAT ,S such that
A6: for x1 being set st x1 in RAT holds
S₁[x1,G . x1] from FUNCT_2:sch 1(A2);
A7: for p being Rational holds G . p = (A /\ (less_dom f,(R_EAL p))) /\ (A /\ (less_dom g,(R_EAL (r - p))))

proof

let p be Rational; :: thesis: G . p = (A /\ (less_dom f,(R_EAL p))) /\ (A /\ (less_dom g,(R_EAL (r - p))))
A8: p in RAT by RAT_1:def 2;
A9: ex q being Rational st
( q = p & G . p = (A /\ (less_dom f,(R_EAL q))) /\ (A /\ (less_dom g,(R_EAL (r - q)))) ) by A6, A8;
thus G . p = (A /\ (less_dom f,(R_EAL p))) /\ (A /\ (less_dom g,(R_EAL (r - p)))) by A9; :: thesis: verum

end;

take G ; :: thesis: for p being Rational holds G . p = (A /\ (less_dom f,(R_EAL p))) /\ (A /\ (less_dom g,(R_EAL (r - p))))
thus for p being Rational holds G . p = (A /\ (less_dom f,(R_EAL p))) /\ (A /\ (less_dom g,(R_EAL (r - p)))) by A7; :: thesis: verum