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 () & g is () & ( 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 () & g is () & ( 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 () & g is () & ( 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 () & g is () & ( 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 () & g is () & ( 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 () & g is () & ( 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 () and
A2: g is () 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 A1, A2, Th16;
A5: 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
A6: x in Y and
A7: Y in rng F by TARSKI:def 4;
consider p being object 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,p))) /\ (A /\ (less_dom (g,(r - p)))) by A3, A6, A9;
then A11: x in A /\ (less_dom (f,p)) by XBOOLE_0:def 4;
then A12: x in A by XBOOLE_0:def 4;
A13: x in less_dom (f,p) by A11, XBOOLE_0:def 4;
x in A /\ (less_dom (g,(r - p))) by A10, XBOOLE_0:def 4;
then A14: x in less_dom (g,(r - p)) by XBOOLE_0:def 4;
reconsider x = x as Element of X by A10;
f . x < p by A13, MESFUNC1:def 11;
then A15: f . x <> +infty by XXREAL_0:4;
A16: -infty < f . x by A1;
A17: -infty < g . x by A2;
A18: g . x < r - p by A14, MESFUNC1:def 11;
then g . x <> +infty by XXREAL_0:4;
then reconsider f1 = f . x, g1 = g . x as Element of 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) by A20, A22, MESFUNC1:def 11;
hence x in A /\ (less_dom ((f + g),r)) by A12, XBOOLE_0:def 4; :: thesis: verum

end;

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

end;

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