let X be non empty set ; :: thesis: for S being SigmaField of X

for M being sigma_Measure of S

for f, g being PartFunc of X,ExtREAL st ex E0 being Element of S st

( dom (f + g) = E0 & f + g is E0 -measurable ) & f is_integrable_on M & g is_integrable_on M holds

f + g is_integrable_on M

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f, g being PartFunc of X,ExtREAL st ex E0 being Element of S st

( dom (f + g) = E0 & f + g is E0 -measurable ) & f is_integrable_on M & g is_integrable_on M holds

f + g is_integrable_on M

let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,ExtREAL st ex E0 being Element of S st

( dom (f + g) = E0 & f + g is E0 -measurable ) & f is_integrable_on M & g is_integrable_on M holds

f + g is_integrable_on M

let f, g be PartFunc of X,ExtREAL; :: thesis: ( ex E0 being Element of S st

( dom (f + g) = E0 & f + g is E0 -measurable ) & f is_integrable_on M & g is_integrable_on M implies f + g is_integrable_on M )

assume that

A1: ex E0 being Element of S st

( dom (f + g) = E0 & f + g is E0 -measurable ) and

A2: f is_integrable_on M and

A3: g is_integrable_on M ; :: thesis: f + g is_integrable_on M

consider E being Element of S such that

A4: dom (f + g) = E and

A5: f + g is E -measurable by A1;

A6: |.f.| | E is nonnegative by Lm1, Th15;

|.g.| is_integrable_on M by A3, Th100;

then A7: |.g.| | E is_integrable_on M by Th97;

A8: |.g.| | E is nonnegative by Lm1, Th15;

A9: dom (f + g) = ((dom f) /\ (dom g)) \ (((f " {-infty}) /\ (g " {+infty})) \/ ((f " {+infty}) /\ (g " {-infty}))) by MESFUNC1:def 3;

then dom (f + g) c= dom g by XBOOLE_1:18, XBOOLE_1:36;

then A10: E c= dom |.g.| by A4, MESFUNC1:def 10;

then A11: (dom |.g.|) /\ E = E by XBOOLE_1:28;

dom (f + g) c= dom f by A9, XBOOLE_1:18, XBOOLE_1:36;

then A12: E c= dom |.f.| by A4, MESFUNC1:def 10;

then (dom |.f.|) /\ E = E by XBOOLE_1:28;

then A13: E = dom (|.f.| | E) by RELAT_1:61;

then A14: (dom (|.f.| | E)) /\ (dom (|.g.| | E)) = E /\ E by A11, RELAT_1:61;

then A15: dom ((|.f.| | E) + (|.g.| | E)) = E by A6, A8, Th22;

A16: E = dom (|.g.| | E) by A11, RELAT_1:61;

then |.f.| | E is_integrable_on M by Th97;

then (|.f.| | E) + (|.g.| | E) is_integrable_on M by A7, A6, A8, Th106;

hence f + g is_integrable_on M by A4, A5, A17, A15, Th102; :: thesis: verum

for M being sigma_Measure of S

for f, g being PartFunc of X,ExtREAL st ex E0 being Element of S st

( dom (f + g) = E0 & f + g is E0 -measurable ) & f is_integrable_on M & g is_integrable_on M holds

f + g is_integrable_on M

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for f, g being PartFunc of X,ExtREAL st ex E0 being Element of S st

( dom (f + g) = E0 & f + g is E0 -measurable ) & f is_integrable_on M & g is_integrable_on M holds

f + g is_integrable_on M

let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,ExtREAL st ex E0 being Element of S st

( dom (f + g) = E0 & f + g is E0 -measurable ) & f is_integrable_on M & g is_integrable_on M holds

f + g is_integrable_on M

let f, g be PartFunc of X,ExtREAL; :: thesis: ( ex E0 being Element of S st

( dom (f + g) = E0 & f + g is E0 -measurable ) & f is_integrable_on M & g is_integrable_on M implies f + g is_integrable_on M )

assume that

A1: ex E0 being Element of S st

( dom (f + g) = E0 & f + g is E0 -measurable ) and

A2: f is_integrable_on M and

A3: g is_integrable_on M ; :: thesis: f + g is_integrable_on M

consider E being Element of S such that

A4: dom (f + g) = E and

A5: f + g is E -measurable by A1;

A6: |.f.| | E is nonnegative by Lm1, Th15;

|.g.| is_integrable_on M by A3, Th100;

then A7: |.g.| | E is_integrable_on M by Th97;

A8: |.g.| | E is nonnegative by Lm1, Th15;

A9: dom (f + g) = ((dom f) /\ (dom g)) \ (((f " {-infty}) /\ (g " {+infty})) \/ ((f " {+infty}) /\ (g " {-infty}))) by MESFUNC1:def 3;

then dom (f + g) c= dom g by XBOOLE_1:18, XBOOLE_1:36;

then A10: E c= dom |.g.| by A4, MESFUNC1:def 10;

then A11: (dom |.g.|) /\ E = E by XBOOLE_1:28;

dom (f + g) c= dom f by A9, XBOOLE_1:18, XBOOLE_1:36;

then A12: E c= dom |.f.| by A4, MESFUNC1:def 10;

then (dom |.f.|) /\ E = E by XBOOLE_1:28;

then A13: E = dom (|.f.| | E) by RELAT_1:61;

then A14: (dom (|.f.| | E)) /\ (dom (|.g.| | E)) = E /\ E by A11, RELAT_1:61;

then A15: dom ((|.f.| | E) + (|.g.| | E)) = E by A6, A8, Th22;

A16: E = dom (|.g.| | E) by A11, RELAT_1:61;

A17: now :: thesis: for x being Element of X st x in dom (f + g) holds

|.((f + g) . x).| <= ((|.f.| | E) + (|.g.| | E)) . x

|.f.| is_integrable_on M
by A2, Th100;|.((f + g) . x).| <= ((|.f.| | E) + (|.g.| | E)) . x

let x be Element of X; :: thesis: ( x in dom (f + g) implies |.((f + g) . x).| <= ((|.f.| | E) + (|.g.| | E)) . x )

A18: |.((f . x) + (g . x)).| <= |.(f . x).| + |.(g . x).| by EXTREAL1:24;

assume A19: x in dom (f + g) ; :: thesis: |.((f + g) . x).| <= ((|.f.| | E) + (|.g.| | E)) . x

then A20: x in dom ((|.f.| | E) + (|.g.| | E)) by A4, A6, A8, A14, Th22;

|.(f . x).| + |.(g . x).| = (|.f.| . x) + |.(g . x).| by A4, A12, A19, MESFUNC1:def 10

.= (|.f.| . x) + (|.g.| . x) by A4, A10, A19, MESFUNC1:def 10

.= ((|.f.| | E) . x) + (|.g.| . x) by A4, A13, A19, FUNCT_1:47

.= ((|.f.| | E) . x) + ((|.g.| | E) . x) by A4, A16, A19, FUNCT_1:47

.= ((|.f.| | E) + (|.g.| | E)) . x by A20, MESFUNC1:def 3 ;

hence |.((f + g) . x).| <= ((|.f.| | E) + (|.g.| | E)) . x by A19, A18, MESFUNC1:def 3; :: thesis: verum

end;A18: |.((f . x) + (g . x)).| <= |.(f . x).| + |.(g . x).| by EXTREAL1:24;

assume A19: x in dom (f + g) ; :: thesis: |.((f + g) . x).| <= ((|.f.| | E) + (|.g.| | E)) . x

then A20: x in dom ((|.f.| | E) + (|.g.| | E)) by A4, A6, A8, A14, Th22;

|.(f . x).| + |.(g . x).| = (|.f.| . x) + |.(g . x).| by A4, A12, A19, MESFUNC1:def 10

.= (|.f.| . x) + (|.g.| . x) by A4, A10, A19, MESFUNC1:def 10

.= ((|.f.| | E) . x) + (|.g.| . x) by A4, A13, A19, FUNCT_1:47

.= ((|.f.| | E) . x) + ((|.g.| | E) . x) by A4, A16, A19, FUNCT_1:47

.= ((|.f.| | E) + (|.g.| | E)) . x by A20, MESFUNC1:def 3 ;

hence |.((f + g) . x).| <= ((|.f.| | E) + (|.g.| | E)) . x by A19, A18, MESFUNC1:def 3; :: thesis: verum

then |.f.| | E is_integrable_on M by Th97;

then (|.f.| | E) + (|.g.| | E) is_integrable_on M by A7, A6, A8, Th106;

hence f + g is_integrable_on M by A4, A5, A17, A15, Th102; :: thesis: verum