let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let f, g be PartFunc of X,ExtREAL ; :: thesis:
let F be Function of RAT ,S; :: thesis:
let r be Real; :: thesis:
let A be Element of S; :: thesis:
assume that
A1: f is real-valued and
A2: g is real-valued 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:
A4: dom (f + g) = (dom f) /\ (dom g) by A1, Th2;
A5: A /\ (less_dom (f + g),(R_EAL r)) c= union (rng F)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A6: x in A /\ (less_dom (f + g),(R_EAL r)) ; :: thesis:
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;
reconsider x = x as Element of X by A6;
A9: (f . x) + (g . x) < R_EAL r by A8, MESFUNC1:def 3;
A10: ( x in dom f & x in dom g ) by A4, A8, XBOOLE_0:def 4;
then ( |.(f . x).| < +infty & |.(g . x).| < +infty ) by A1, A2, Def1;
then A11: ( - +infty < f . x & f . x < +infty & - +infty < g . x & g . x < +infty ) by EXTREAL2:58;
then A12: f . x < (R_EAL r) - (g . x) by A9, XXREAL_3:63;
A13: ( -infty < f . x & -infty < g . x ) by A11, XXREAL_3:23;
then reconsider f1 = f . x as Real by A11, XXREAL_0:14;
reconsider g1 = g . x as Real by A11, A13, XXREAL_0:14;
(R_EAL r) - (g . x) = r - g1 by SUPINF_2:5;
then consider p being Rational such that
A14: ( f1 < p & p < r - g1 ) by A12, RAT_1:22;
( not p <= f1 & not r - p <= g1 ) by A14, XREAL_1:14;
then ( x in less_dom f,(R_EAL p) & x in less_dom g,(R_EAL (r - p)) ) by A10, 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 A15: 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, A15, FUNCT_1:def 5;
then consider Y being set such that
A16: ( x in Y & Y in rng F ) ;
thus x in union (rng F) by A16, TARSKI:def 4; :: thesis:

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in union (rng F) ; :: thesis:
then consider Y being set such that
A17: ( x in Y & Y in rng F ) by TARSKI:def 4;
consider p being set such that
A18: ( p in dom F & Y = F . p ) by A17, FUNCT_1:def 5;
reconsider p = p as Rational by A18;
A19: x in (A /\ (less_dom f,(R_EAL p))) /\ (A /\ (less_dom g,(R_EAL (r - p)))) by A3, A17, A18;
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 A20: ( 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;
then A21: ( x in dom f & f . x < R_EAL p & x in dom g & g . x < R_EAL (r - p) ) by MESFUNC1:def 12;
reconsider x = x as Element of X by A19;
A22: g . x < R_EAL (r - p) by A20, MESFUNC1:def 12;
( |.(f . x).| < +infty & |.(g . x).| < +infty ) by A1, A2, A21, Def1;
then ( - +infty < f . x & f . x < +infty & - +infty < g . x & g . x < +infty ) by EXTREAL2:58;
then A23: ( -infty < f . x & f . x < +infty & -infty < g . x & g . x < +infty ) by XXREAL_3:23;
then reconsider f1 = f . x as Real by XXREAL_0:14;
reconsider g1 = g . x as Real by A23, XXREAL_0:14;
( f1 < p & p < r - g1 ) by A20, A22, MESFUNC1:def 12, XREAL_1:14;
then f1 < r - g1 by XXREAL_0:2;
then A24: f1 + g1 < r by XREAL_1:22;
A25: x in dom (f + g) by A4, A21, 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 A24, A25, MESFUNC1:def 12;
hence x in A /\ (less_dom (f + g),(R_EAL r)) by A20, XBOOLE_0:def 4; :: thesis:

end;

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