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;

A17: now :: thesis: for x being Element of X st x in dom (f + g) holds
|.((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;

|.f.| is_integrable_on M by A2, Th100;
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