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_measurable_on E0 ) & 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_measurable_on E0 ) & 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_measurable_on E0 ) & 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_measurable_on E0 ) & 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_measurable_on E0 ) 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_measurable_on E by A1;
A6: |.f.| | E is nonnegative by Lm1, Th21;
ex E2 being Element of S st
( E2 = dom g & g is_measurable_on E2 ) by A3, Def17;
then |.g.| is_integrable_on M by A3, Th106;
then A7: |.g.| | E is_integrable_on M by Th103;
A8: |.g.| | E is nonnegative by Lm1, Th21;
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, Th28;
A16: E = dom (|.g.| | E) by A11, RELAT_1:61;

A17: now

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 EXTREAL2:13;
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, Th28;
|.(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;

ex E1 being Element of S st
( E1 = dom f & f is_measurable_on E1 ) by A2, Def17;
then |.f.| is_integrable_on M by A2, Th106;
then |.f.| | E is_integrable_on M by Th103;
then (|.f.| | E) + (|.g.| | E) is_integrable_on M by A7, A6, A8, Th112;
hence f + g is_integrable_on M by A4, A5, A17, A15, Th108; :: thesis: verum