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 V82() & g is V82() & ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) holds
A /\ (less_dom ((f + g),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 V82() & g is V82() & ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) holds
A /\ (less_dom ((f + g),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 V82() & g is V82() & ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) holds
A /\ (less_dom ((f + g),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 V82() & g is V82() & ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) holds
A /\ (less_dom ((f + g),r)) = union (rng F)

let r be Real; :: thesis: for A being Element of S st f is V82() & g is V82() & ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) holds
A /\ (less_dom ((f + g),r)) = union (rng F)

let A be Element of S; :: thesis: ( f is V82() & g is V82() & ( for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ) implies A /\ (less_dom ((f + g),r)) = union (rng F) )
assume that
A1: f is V82() and
A2: g is V82() and
A3: for p being Rational holds F . p = (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) ; :: thesis: A /\ (less_dom ((f + g),r)) = union (rng F)
A4: dom (f + g) = (dom f) /\ (dom g) by ;
A5: A /\ (less_dom ((f + g),r)) c= union (rng F)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A /\ (less_dom ((f + g),r)) or x in union (rng F) )
assume A6: x in A /\ (less_dom ((f + g),r)) ; :: thesis: x in union (rng F)
then A7: x in A by XBOOLE_0:def 4;
A8: x in less_dom ((f + g),r) by ;
then A9: x in dom (f + g) by MESFUNC1:def 11;
A10: (f + g) . x < r by ;
reconsider x = x as Element of X by A6;
A11: (f . x) + (g . x) < r by ;
A12: x in dom f by ;
A13: x in dom g by ;
A14: |.(f . x).| < +infty by ;
A15: |.(g . x).| < +infty by ;
A16: - +infty < f . x by ;
A17: f . x < +infty by ;
A18: - +infty < g . x by ;
A19: g . x < +infty by ;
then A20: f . x < r - (g . x) by ;
A21: -infty < f . x by ;
A22: -infty < g . x by ;
reconsider f1 = f . x as Element of REAL by ;
reconsider g1 = g . x as Element of REAL by ;
reconsider rr = r as R_eal by XXREAL_0:def 1;
f1 < r - g1 by ;
then consider p being Rational such that
A23: f1 < p and
A24: p < r - g1 by RAT_1:7;
A25: not r - p <= g1 by ;
A26: x in less_dom (f,p) by ;
A27: x in less_dom (g,(r - p)) by ;
A28: x in A /\ (less_dom (f,p)) by ;
x in A /\ (less_dom (g,(r - p))) by ;
then A29: x in (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) by ;
p in RAT by RAT_1:def 2;
then A30: p in dom F by FUNCT_2:def 1;
A31: x in F . p by ;
F . p in rng F by ;
hence x in union (rng F) by ; :: thesis: verum
end;
union (rng F) c= A /\ (less_dom ((f + g),r))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (rng F) or x in A /\ (less_dom ((f + g),r)) )
assume x in union (rng F) ; :: thesis: x in A /\ (less_dom ((f + g),r))
then consider Y being set such that
A32: x in Y and
A33: Y in rng F by TARSKI:def 4;
consider p being object such that
A34: p in dom F and
A35: Y = F . p by ;
reconsider p = p as Rational by A34;
A36: x in (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) by A3, A32, A35;
then A37: x in A /\ (less_dom (f,p)) by XBOOLE_0:def 4;
A38: x in A /\ (less_dom (g,(r - p))) by ;
A39: x in A by ;
A40: x in less_dom (f,p) by ;
A41: x in less_dom (g,(r - p)) by ;
A42: x in dom f by ;
A43: x in dom g by ;
reconsider x = x as Element of X by A36;
A44: g . x < r - p by ;
A45: |.(f . x).| < +infty by ;
A46: |.(g . x).| < +infty by ;
A47: - +infty < f . x by ;
A48: - +infty < g . x by ;
A49: -infty < f . x by ;
A50: f . x < +infty by ;
A51: -infty < g . x by ;
A52: g . x < +infty by ;
reconsider f1 = f . x as Element of REAL by ;
reconsider g1 = g . x as Element of REAL by ;
A53: f1 < p by ;
p < r - g1 by ;
then f1 < r - g1 by ;
then A54: f1 + g1 < r by XREAL_1:20;
A55: x in dom (f + g) by ;
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) by ;
hence x in A /\ (less_dom ((f + g),r)) by ; :: thesis: verum
end;
hence A /\ (less_dom ((f + g),r)) = union (rng F) by A5; :: thesis: verum