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 A1, Th2;

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

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 A1, Th2;

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

proof

union (rng F) c= A /\ (less_dom ((f + g),r))
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 A6, XBOOLE_0:def 4;

then A9: x in dom (f + g) by MESFUNC1:def 11;

A10: (f + g) . x < r by A8, MESFUNC1:def 11;

reconsider x = x as Element of X by A6;

A11: (f . x) + (g . x) < r by A9, A10, MESFUNC1:def 3;

A12: x in dom f by A4, A9, XBOOLE_0:def 4;

A13: x in dom g by A4, A9, XBOOLE_0:def 4;

A14: |.(f . x).| < +infty by A1, A12;

A15: |.(g . x).| < +infty by A2, A13;

A16: - +infty < f . x by A14, EXTREAL1:21;

A17: f . x < +infty by A14, EXTREAL1:21;

A18: - +infty < g . x by A15, EXTREAL1:21;

A19: g . x < +infty by A15, EXTREAL1:21;

then A20: f . x < r - (g . x) by A11, A17, XXREAL_3:52;

A21: -infty < f . x by A16, XXREAL_3:23;

A22: -infty < g . x by A18, XXREAL_3:23;

reconsider f1 = f . x as Element of REAL by A17, A21, XXREAL_0:14;

reconsider g1 = g . x as Element of REAL by A19, A22, XXREAL_0:14;

reconsider rr = r as R_eal by XXREAL_0:def 1;

f1 < r - g1 by A20, SUPINF_2:3;

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 A24, XREAL_1:12;

A26: x in less_dom (f,p) by A12, A23, MESFUNC1:def 11;

A27: x in less_dom (g,(r - p)) by A13, A25, MESFUNC1:def 11;

A28: x in A /\ (less_dom (f,p)) by A7, A26, XBOOLE_0:def 4;

x in A /\ (less_dom (g,(r - p))) by A7, A27, XBOOLE_0:def 4;

then A29: x in (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) by A28, XBOOLE_0:def 4;

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 A3, A29;

F . p in rng F by A30, FUNCT_1:def 3;

hence x in union (rng F) by A31, TARSKI:def 4; :: thesis: verum

end;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 A6, XBOOLE_0:def 4;

then A9: x in dom (f + g) by MESFUNC1:def 11;

A10: (f + g) . x < r by A8, MESFUNC1:def 11;

reconsider x = x as Element of X by A6;

A11: (f . x) + (g . x) < r by A9, A10, MESFUNC1:def 3;

A12: x in dom f by A4, A9, XBOOLE_0:def 4;

A13: x in dom g by A4, A9, XBOOLE_0:def 4;

A14: |.(f . x).| < +infty by A1, A12;

A15: |.(g . x).| < +infty by A2, A13;

A16: - +infty < f . x by A14, EXTREAL1:21;

A17: f . x < +infty by A14, EXTREAL1:21;

A18: - +infty < g . x by A15, EXTREAL1:21;

A19: g . x < +infty by A15, EXTREAL1:21;

then A20: f . x < r - (g . x) by A11, A17, XXREAL_3:52;

A21: -infty < f . x by A16, XXREAL_3:23;

A22: -infty < g . x by A18, XXREAL_3:23;

reconsider f1 = f . x as Element of REAL by A17, A21, XXREAL_0:14;

reconsider g1 = g . x as Element of REAL by A19, A22, XXREAL_0:14;

reconsider rr = r as R_eal by XXREAL_0:def 1;

f1 < r - g1 by A20, SUPINF_2:3;

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 A24, XREAL_1:12;

A26: x in less_dom (f,p) by A12, A23, MESFUNC1:def 11;

A27: x in less_dom (g,(r - p)) by A13, A25, MESFUNC1:def 11;

A28: x in A /\ (less_dom (f,p)) by A7, A26, XBOOLE_0:def 4;

x in A /\ (less_dom (g,(r - p))) by A7, A27, XBOOLE_0:def 4;

then A29: x in (A /\ (less_dom (f,p))) /\ (A /\ (less_dom (g,(r - p)))) by A28, XBOOLE_0:def 4;

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 A3, A29;

F . p in rng F by A30, FUNCT_1:def 3;

hence x in union (rng F) by A31, TARSKI:def 4; :: thesis: verum

proof

hence
A /\ (less_dom ((f + g),r)) = union (rng F)
by A5; :: thesis: verum
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 A33, FUNCT_1:def 3;

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 A36, XBOOLE_0:def 4;

A39: x in A by A37, XBOOLE_0:def 4;

A40: x in less_dom (f,p) by A37, XBOOLE_0:def 4;

A41: x in less_dom (g,(r - p)) by A38, XBOOLE_0:def 4;

A42: x in dom f by A40, MESFUNC1:def 11;

A43: x in dom g by A41, MESFUNC1:def 11;

reconsider x = x as Element of X by A36;

A44: g . x < r - p by A41, MESFUNC1:def 11;

A45: |.(f . x).| < +infty by A1, A42;

A46: |.(g . x).| < +infty by A2, A43;

A47: - +infty < f . x by A45, EXTREAL1:21;

A48: - +infty < g . x by A46, EXTREAL1:21;

A49: -infty < f . x by A47, XXREAL_3:23;

A50: f . x < +infty by A45, EXTREAL1:21;

A51: -infty < g . x by A48, XXREAL_3:23;

A52: g . x < +infty by A46, EXTREAL1:21;

reconsider f1 = f . x as Element of REAL by A49, A50, XXREAL_0:14;

reconsider g1 = g . x as Element of REAL by A51, A52, XXREAL_0:14;

A53: f1 < p by A40, MESFUNC1:def 11;

p < r - g1 by A44, XREAL_1:12;

then f1 < r - g1 by A53, XXREAL_0:2;

then A54: f1 + g1 < r by XREAL_1:20;

A55: x in dom (f + g) by A4, A42, A43, 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 A54, A55, MESFUNC1:def 11;

hence x in A /\ (less_dom ((f + g),r)) by A39, XBOOLE_0:def 4; :: thesis: verum

end;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 A33, FUNCT_1:def 3;

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 A36, XBOOLE_0:def 4;

A39: x in A by A37, XBOOLE_0:def 4;

A40: x in less_dom (f,p) by A37, XBOOLE_0:def 4;

A41: x in less_dom (g,(r - p)) by A38, XBOOLE_0:def 4;

A42: x in dom f by A40, MESFUNC1:def 11;

A43: x in dom g by A41, MESFUNC1:def 11;

reconsider x = x as Element of X by A36;

A44: g . x < r - p by A41, MESFUNC1:def 11;

A45: |.(f . x).| < +infty by A1, A42;

A46: |.(g . x).| < +infty by A2, A43;

A47: - +infty < f . x by A45, EXTREAL1:21;

A48: - +infty < g . x by A46, EXTREAL1:21;

A49: -infty < f . x by A47, XXREAL_3:23;

A50: f . x < +infty by A45, EXTREAL1:21;

A51: -infty < g . x by A48, XXREAL_3:23;

A52: g . x < +infty by A46, EXTREAL1:21;

reconsider f1 = f . x as Element of REAL by A49, A50, XXREAL_0:14;

reconsider g1 = g . x as Element of REAL by A51, A52, XXREAL_0:14;

A53: f1 < p by A40, MESFUNC1:def 11;

p < r - g1 by A44, XREAL_1:12;

then f1 < r - g1 by A53, XXREAL_0:2;

then A54: f1 + g1 < r by XREAL_1:20;

A55: x in dom (f + g) by A4, A42, A43, 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 A54, A55, MESFUNC1:def 11;

hence x in A /\ (less_dom ((f + g),r)) by A39, XBOOLE_0:def 4; :: thesis: verum