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 A1: ( 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 ) ; :: thesis: f + g is_integrable_on M
then consider E being Element of S such that
A2: ( dom (f + g) = E & f + g is_measurable_on E ) ;
A3: dom (f + g) = ((dom f) /\ (dom g)) \ (((f " {-infty }) /\ (g " {+infty })) \/ ((f " {+infty }) /\ (g " {-infty }))) by MESFUNC1:def 3;
then A4: dom (f + g) c= (dom f) /\ (dom g) by XBOOLE_1:36;
( dom (f + g) c= dom f & dom (f + g) c= dom g ) by A3, XBOOLE_1:18, XBOOLE_1:36;
then A5: ( E c= dom |.f.| & E c= dom |.g.| ) by A2, MESFUNC1:def 10;
consider E1 being Element of S such that
A6: ( E1 = dom f & f is_measurable_on E1 ) by A1, Def17;
consider E2 being Element of S such that
A7: ( E2 = dom g & g is_measurable_on E2 ) by A1, Def17;
( |.f.| is_integrable_on M & |.g.| is_integrable_on M ) by A1, A6, A7, Th106;
then A8: ( |.f.| | E is_integrable_on M & |.g.| | E is_integrable_on M ) by Th103;
( f is_measurable_on E & g is_measurable_on E ) by A2, A4, A6, A7, MESFUNC1:34, XBOOLE_1:18;
then A9: ( |.f.| is_measurable_on E & |.g.| is_measurable_on E ) by A2, A4, MESFUNC2:29, XBOOLE_1:18;
A10: ( |.f.| | E is nonnegative & |.g.| | E is nonnegative ) by Th21, Lm1;
then A11: (|.f.| | E) + (|.g.| | E) is_integrable_on M by A8, Th112;
( (dom |.f.|) /\ E = E & (dom |.g.|) /\ E = E ) by A5, XBOOLE_1:28;
then A12: ( E = dom (|.f.| | E) & |.f.| | E is_measurable_on E & E = dom (|.g.| | E) & |.g.| | E is_measurable_on E ) by A9, Th48, RELAT_1:90;
then A13: (dom (|.f.| | E)) /\ (dom (|.g.| | E)) = E /\ E ;
for x being set st x in dom f holds
f . x in ExtREAL ;
then reconsider ff = f as Function of (dom f),ExtREAL by FUNCT_2:5;
for x being set st x in dom g holds
g . x in ExtREAL ;
then reconsider gg = g as Function of (dom g),ExtREAL by FUNCT_2:5;

A14: now

let x be Element of X; :: thesis: ( x in dom (f + g) implies |.((f + g) . x).| <= ((|.f.| | E) + (|.g.| | E)) . x )
assume A15: x in dom (f + g) ; :: thesis: |.((f + g) . x).| <= ((|.f.| | E) + (|.g.| | E)) . x
then ( x in dom |.f.| & x in dom |.g.| ) by A2, A5;
then A16: ( x in dom ff & x in dom gg ) by MESFUNC1:def 10;
A17: x in dom ((|.f.| | E) + (|.g.| | E)) by A2, A10, A13, A15, Th28;
( not ( f . x = +infty & g . x = -infty ) & not ( f . x = -infty & g . x = +infty ) )

proof

assume A18: ( ( f . x = +infty & g . x = -infty ) or ( f . x = -infty & g . x = +infty ) ) ; :: thesis: contradiction

per cases ( ( f . x = +infty & g . x = -infty ) or ( f . x = -infty & g . x = +infty ) ) by A18;

suppose ( f . x = +infty & g . x = -infty ) ; :: thesis: contradiction

then ( ff . x in {+infty } & gg . x in {-infty } ) by TARSKI:def 1;
then ( x in ff " {+infty } & x in gg " {-infty } ) by A16, FUNCT_2:46;
then A19: x in (ff " {+infty }) /\ (gg " {-infty }) by XBOOLE_0:def 4;
(ff " {+infty }) /\ (gg " {-infty }) c= ((ff " {+infty }) /\ (gg " {-infty })) \/ ((ff " {-infty }) /\ (gg " {+infty })) by XBOOLE_1:7;
hence contradiction by A3, A15, A19, XBOOLE_0:def 5; :: thesis: verum

end;

suppose ( f . x = -infty & g . x = +infty ) ; :: thesis: contradiction

then ( ff . x in {-infty } & gg . x in {+infty } ) by TARSKI:def 1;
then ( x in ff " {-infty } & x in gg " {+infty } ) by A16, FUNCT_2:46;
then A20: x in (ff " {-infty }) /\ (gg " {+infty }) by XBOOLE_0:def 4;
(ff " {-infty }) /\ (gg " {+infty }) c= ((ff " {+infty }) /\ (gg " {-infty })) \/ ((ff " {-infty }) /\ (gg " {+infty })) by XBOOLE_1:7;
hence contradiction by A3, A15, A20, XBOOLE_0:def 5; :: thesis: verum

end;

end;

end;

then A21: |.((f . x) + (g . x)).| <= |.(f . x).| + |.(g . x).| by EXTREAL2:61;
|.(f . x).| + |.(g . x).| = (|.f.| . x) + |.(g . x).| by A2, A5, A15, MESFUNC1:def 10
.= (|.f.| . x) + (|.g.| . x) by A2, A5, A15, MESFUNC1:def 10
.= ((|.f.| | E) . x) + (|.g.| . x) by A2, A12, A15, FUNCT_1:70
.= ((|.f.| | E) . x) + ((|.g.| | E) . x) by A2, A12, A15, FUNCT_1:70
.= ((|.f.| | E) + (|.g.| | E)) . x by A17, MESFUNC1:def 3 ;
hence |.((f + g) . x).| <= ((|.f.| | E) + (|.g.| | E)) . x by A15, A21, MESFUNC1:def 3; :: thesis: verum

end;

dom ((|.f.| | E) + (|.g.| | E)) = E by A10, A13, Th28;
hence f + g is_integrable_on M by A2, A11, A14, Th108; :: thesis: verum