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

proof

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

end;

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

proof

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

end;

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