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: 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
A6: x in Y and
A7: Y in rng F by TARSKI:def 4;
consider p being set such that
A8: p in dom F and
A9: Y = F . p by A7, FUNCT_1:def 3;
reconsider p = p as Rational by A8;
A10: x in (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) by A3, A6, A9;
then A11: x in A /\ (less_dom (f,(R_EAL p))) by XBOOLE_0:def 4;
then A12: x in A by XBOOLE_0:def 4;
A13: x in less_dom (f,(R_EAL p)) by A11, XBOOLE_0:def 4;
x in A /\ (less_dom (g,(R_EAL (r - p)))) by A10, XBOOLE_0:def 4;
then A14: x in less_dom (g,(R_EAL (r - p))) by XBOOLE_0:def 4;
reconsider x = x as Element of X by A10;
f . x < R_EAL p by A13, MESFUNC1:def 11;
then A15: f . x <> +infty by XXREAL_0:4;
A16: -infty < f . x by A1, Def5;
A17: -infty < g . x by A2, Def5;
A18: g . x < R_EAL (r - p) by A14, MESFUNC1:def 11;
then g . x <> +infty by XXREAL_0:4;
then reconsider f1 = f . x, g1 = g . x as Real by A16, A17, A15, XXREAL_0:14;
A19: p < r - g1 by A18, XREAL_1:12;
f1 < p by A13, MESFUNC1:def 11;
then f1 < r - g1 by A19, XXREAL_0:2;
then A20: f1 + g1 < r by XREAL_1:20;
A21: x in dom g by A14, MESFUNC1:def 11;
x in dom f by A13, MESFUNC1:def 11;
then A22: 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 A20, A22, MESFUNC1:def 11;
hence x in A /\ (less_dom ((f + g),(R_EAL r))) by A12, XBOOLE_0:def 4; :: thesis: verum

end;

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 A23: x in A /\ (less_dom ((f + g),(R_EAL r))) ; :: thesis: x in union (rng F)
then A24: x in A by XBOOLE_0:def 4;
A25: x in less_dom ((f + g),(R_EAL r)) by A23, XBOOLE_0:def 4;
then A26: x in dom (f + g) by MESFUNC1:def 11;
then A27: x in dom f by A4, XBOOLE_0:def 4;
A28: (f + g) . x < R_EAL r by A25, MESFUNC1:def 11;
A29: x in dom g by A4, A26, XBOOLE_0:def 4;
reconsider x = x as Element of X by A23;
A30: -infty < f . x by A1, Def5;
A31: (f . x) + (g . x) < R_EAL r by A26, A28, MESFUNC1:def 3;
then A32: g . x <> +infty by A30, XXREAL_3:52;
A33: -infty < g . x by A2, Def5;
then f . x <> +infty by A31, XXREAL_3:52;
then reconsider f1 = f . x, g1 = g . x as Real by A30, A33, A32, XXREAL_0:14;
A34: (R_EAL r) - (g . x) = r - g1 by SUPINF_2:3;
f . x < (R_EAL r) - (g . x) by A31, A30, A33, XXREAL_3:52;
then consider p being Rational such that
A35: f1 < p and
A36: p < r - g1 by A34, RAT_1:7;
not r - p <= g1 by A36, XREAL_1:12;
then x in less_dom (g,(R_EAL (r - p))) by A29, MESFUNC1:def 11;
then A37: x in A /\ (less_dom (g,(R_EAL (r - p)))) by A24, XBOOLE_0:def 4;
p in RAT by RAT_1:def 2;
then p in dom F by FUNCT_2:def 1;
then A38: F . p in rng F by FUNCT_1:def 3;
x in less_dom (f,(R_EAL p)) by A27, A35, MESFUNC1:def 11;
then x in A /\ (less_dom (f,(R_EAL p))) by A24, XBOOLE_0:def 4;
then x in (A /\ (less_dom (f,(R_EAL p)))) /\ (A /\ (less_dom (g,(R_EAL (r - p))))) by A37, XBOOLE_0:def 4;
then x in F . p by A3;
hence x in union (rng F) by A38, TARSKI: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