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 f is_integrable_on M & g is_integrable_on M holds
ex E being Element of S st
( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M holds
ex E being Element of S st
( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) )
let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M holds
ex E being Element of S st
( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) )
let f, g be PartFunc of X,ExtREAL; :: thesis: ( f is_integrable_on M & g is_integrable_on M implies ex E being Element of S st
( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) ) )
assume that
A1: f is_integrable_on M and
A2: g is_integrable_on M ; :: thesis: ex E being Element of S st
( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) )
A3: |.g.| is_integrable_on M by A2, MESFUNC5:100;
A4: f + g is_integrable_on M by A1, A2, MESFUNC5:108;
A5: |.(f + g).| is_integrable_on M by A4, MESFUNC5:100;
for x being Element of X st x in dom |.(f + g).| holds
|.(f + g).| . x <= (|.f.| + |.g.|) . x by Th21;
then A6: (|.f.| + |.g.|) - |.(f + g).| is nonnegative by Th1;
set G = |.g.|;
set F = |.f.|;
A7: dom |.(f + g).| = dom (f + g) by MESFUNC1:def 10
.= ((dom f) /\ (dom g)) \ (((f " {-infty}) /\ (g " {+infty})) \/ ((f " {+infty}) /\ (g " {-infty}))) by MESFUNC1:def 3 ;
A8: |.f.| is_integrable_on M by A1, MESFUNC5:100;
then |.f.| + |.g.| is_integrable_on M by A3, MESFUNC5:108;
then consider E being Element of S such that
A9: E = (dom (|.f.| + |.g.|)) /\ (dom |.(f + g).|) and
A10: Integral (M,(|.(f + g).| | E)) <= Integral (M,((|.f.| + |.g.|) | E)) by A5, A6, Th3;
A11: |.g.| | E is_integrable_on M by A3, MESFUNC5:97;
|.f.| | E is_integrable_on M by A8, MESFUNC5:97;
then consider E1 being Element of S such that
A12: E1 = (dom (|.f.| | E)) /\ (dom (|.g.| | E)) and
A13: Integral (M,((|.f.| | E) + (|.g.| | E))) = (Integral (M,((|.f.| | E) | E1))) + (Integral (M,((|.g.| | E) | E1))) by A11, MESFUNC5:109;
take E ; :: thesis: ( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) )
dom (|.g.| | E) = (dom |.g.|) /\ E by RELAT_1:61;
then A14: dom (|.g.| | E) = (dom g) /\ E by MESFUNC1:def 10;
A15: dom (|.f.| + |.g.|) = (dom f) /\ (dom g) by Th19;
then A16: E = dom |.(f + g).| by A9, A7, XBOOLE_1:28, XBOOLE_1:36;
dom (|.f.| | E) = (dom |.f.|) /\ E by RELAT_1:61;
then dom (|.f.| | E) = (dom f) /\ E by MESFUNC1:def 10;
then E1 = (((dom f) /\ E) /\ E) /\ (dom g) by A12, A14, XBOOLE_1:16;
then E1 = ((dom f) /\ (E /\ E)) /\ (dom g) by XBOOLE_1:16;
then E1 = ((dom f) /\ (dom g)) /\ E by XBOOLE_1:16;
then A17: E1 = E by A9, A15, A7, XBOOLE_1:28, XBOOLE_1:36;
then A18: (|.g.| | E) | E1 = |.g.| | E by FUNCT_1:51;
(|.f.| | E) | E1 = |.f.| | E by A17, FUNCT_1:51;
hence ( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) ) by A10, A13, A16, A18, Th20, MESFUNC1:def 10; :: thesis: verum