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_{1}[ 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_{1}[x1,y1] )

A5: for x1 being object st x1 in RAT holds

S_{1}[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))))

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

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

( 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

proof

consider G being Function of RAT,S such that
let x1 be object ; :: thesis: ( x1 in RAT implies ex y1 being object st

( y1 in S & S_{1}[x1,y1] ) )

assume x1 in RAT ; :: thesis: ex y1 being object st

( y1 in S & S_{1}[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_{1}[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_{1}[x1,(A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p))))] )
by A3, A4, FINSUB_1:def 2; :: thesis: verum

end;( y1 in S & S

assume x1 in RAT ; :: thesis: ex y1 being object st

( y1 in S & S

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

thus ( (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) in S & S

A5: for x1 being object st x1 in RAT holds

S

A6: for p being Rational holds G . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p))))

proof

take
G
; :: thesis: for p being Rational holds G . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p))))
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;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

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