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 x1 in RAT ; :: thesis: ex y1 being set st
( y1 in S & S₁[x1,y1] )
then consider p being Rational such that
A4: p = x1 ;
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)))))
p in RAT by RAT_1:def 2;
then 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;
hence G . p = (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) ; :: 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