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))

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

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

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 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;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