let X be non empty set ; :: thesis: for S being SigmaField of X
for f, g being PartFunc of X,ExtREAL
for F being Function of RAT ,S
for r being Real
for A being Element of S st f is without-infty & g is without-infty & ( for p being Rational holds F . p = (A /\ (less_dom f,(R_EAL p))) /\ (A /\ (less_dom g,(R_EAL (r - p)))) ) holds
A /\ (less_dom (f + g),(R_EAL r)) = union (rng F)
let S be SigmaField of X; :: thesis: for f, g being PartFunc of X,ExtREAL
for F being Function of RAT ,S
for r being Real
for A being Element of S st f is without-infty & g is without-infty & ( for p being Rational holds F . p = (A /\ (less_dom f,(R_EAL p))) /\ (A /\ (less_dom g,(R_EAL (r - p)))) ) holds
A /\ (less_dom (f + g),(R_EAL r)) = union (rng F)
let f, g be PartFunc of X,ExtREAL ; :: thesis: for F being Function of RAT ,S
for r being Real
for A being Element of S st f is without-infty & g is without-infty & ( for p being Rational holds F . p = (A /\ (less_dom f,(R_EAL p))) /\ (A /\ (less_dom g,(R_EAL (r - p)))) ) holds
A /\ (less_dom (f + g),(R_EAL r)) = union (rng F)
let F be Function of RAT ,S; :: thesis: for r being Real
for A being Element of S st f is without-infty & g is without-infty & ( for p being Rational holds F . p = (A /\ (less_dom f,(R_EAL p))) /\ (A /\ (less_dom g,(R_EAL (r - p)))) ) holds
A /\ (less_dom (f + g),(R_EAL r)) = union (rng F)
let r be Real; :: thesis: for A being Element of S st f is without-infty & g is without-infty & ( for p being Rational holds F . p = (A /\ (less_dom f,(R_EAL p))) /\ (A /\ (less_dom g,(R_EAL (r - p)))) ) holds
A /\ (less_dom (f + g),(R_EAL r)) = union (rng F)
let A be Element of S; :: thesis: ( f is without-infty & g is without-infty & ( for p being Rational holds F . p = (A /\ (less_dom f,(R_EAL p))) /\ (A /\ (less_dom g,(R_EAL (r - p)))) ) implies A /\ (less_dom (f + g),(R_EAL r)) = union (rng F) )
assume that
A1: f is without-infty and
A2: g is without-infty and
A3: for p being Rational holds F . p = (A /\ (less_dom f,(R_EAL p))) /\ (A /\ (less_dom g,(R_EAL (r - p)))) ; :: thesis: A /\ (less_dom (f + g),(R_EAL r)) = union (rng F)
A4: dom (f + g) = (dom f) /\ (dom g) by A1, A2, Th22;
A5: A /\ (less_dom (f + g),(R_EAL r)) c= union (rng F)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A /\ (less_dom (f + g),(R_EAL r)) or x in union (rng F) )
assume A6: x in A /\ (less_dom (f + g),(R_EAL r)) ; :: thesis: x in union (rng F)
then A7: ( x in A & x in less_dom (f + g),(R_EAL r) ) by XBOOLE_0:def 4;
then A8: ( x in dom (f + g) & (f + g) . x < R_EAL r ) by MESFUNC1:def 12;
then A9: ( x in dom f & x in dom g ) by A4, XBOOLE_0:def 4;
reconsider x = x as Element of X by A6;
A10: (f . x) + (g . x) < R_EAL r by A8, MESFUNC1:def 3;
A11: ( -infty < f . x & -infty < g . x ) by A1, A2, Def5;
then A12: ( f . x < (R_EAL r) - (g . x) & f . x <> +infty & g . x <> +infty ) by A10, XXREAL_3:63;
then reconsider f1 = f . x, g1 = g . x as Real by A11, XXREAL_0:14;
(R_EAL r) - (g . x) = r - g1 by SUPINF_2:5;
then consider p being Rational such that
A13: ( f1 < p & p < r - g1 ) by A12, RAT_1:22;
( not p <= f1 & not r - p <= g1 ) by A13, XREAL_1:14;
then ( x in less_dom f,(R_EAL p) & x in less_dom g,(R_EAL (r - p)) ) by A9, MESFUNC1:def 12;
then ( x in A /\ (less_dom f,(R_EAL p)) & x in A /\ (less_dom g,(R_EAL (r - p))) ) by A7, XBOOLE_0:def 4;
then A14: x in (A /\ (less_dom f,(R_EAL p))) /\ (A /\ (less_dom g,(R_EAL (r - p)))) by XBOOLE_0:def 4;
p in RAT by RAT_1:def 2;
then p in dom F by FUNCT_2:def 1;
then ( x in F . p & F . p in rng F ) by A3, A14, FUNCT_1:def 5;
hence x in union (rng F) by TARSKI:def 4; :: thesis: verum

end;

union (rng F) c= A /\ (less_dom (f + g),(R_EAL r))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union (rng F) or x in A /\ (less_dom (f + g),(R_EAL r)) )
assume x in union (rng F) ; :: thesis: x in A /\ (less_dom (f + g),(R_EAL r))
then consider Y being set such that
A15: ( x in Y & Y in rng F ) by TARSKI:def 4;
consider p being set such that
A16: ( p in dom F & Y = F . p ) by A15, FUNCT_1:def 5;
reconsider p = p as Rational by A16;
A17: x in (A /\ (less_dom f,(R_EAL p))) /\ (A /\ (less_dom g,(R_EAL (r - p)))) by A3, A15, A16;
then ( x in A /\ (less_dom f,(R_EAL p)) & x in A /\ (less_dom g,(R_EAL (r - p))) ) by XBOOLE_0:def 4;
then A18: ( x in A & x in less_dom f,(R_EAL p) & x in less_dom g,(R_EAL (r - p)) ) by XBOOLE_0:def 4;
reconsider x = x as Element of X by A17;
A19: f . x < R_EAL p by A18, MESFUNC1:def 12;
A20: g . x < R_EAL (r - p) by A18, MESFUNC1:def 12;
A21: ( -infty < f . x & -infty < g . x ) by A1, A2, Def5;
( f . x <> +infty & g . x <> +infty ) by A19, A20, XXREAL_0:4;
then reconsider f1 = f . x, g1 = g . x as Real by A21, XXREAL_0:14;
( f1 < p & p < r - g1 ) by A18, A20, MESFUNC1:def 12, XREAL_1:14;
then f1 < r - g1 by XXREAL_0:2;
then A22: f1 + g1 < r by XREAL_1:22;
( x in dom f & x in dom g ) by A18, MESFUNC1:def 12;
then A23: x in dom (f + g) by A4, XBOOLE_0:def 4;
then (f + g) . x = (f . x) + (g . x) by MESFUNC1:def 3
.= f1 + g1 by SUPINF_2:1 ;
then x in less_dom (f + g),(R_EAL r) by A22, A23, MESFUNC1:def 12;
hence x in A /\ (less_dom (f + g),(R_EAL r)) by A18, XBOOLE_0:def 4; :: thesis: verum

end;

hence A /\ (less_dom (f + g),(R_EAL r)) = union (rng F) by A5, XBOOLE_0:def 10; :: thesis: verum