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 A1: ( f is_integrable_on M & 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)) )
then ( ex A being Element of S st
( A = dom f & f is_measurable_on A ) & ex A being Element of S st
( A = dom g & g is_measurable_on A ) ) by MESFUNC5:def 17;
then A2: ( |.f.| is_integrable_on M & |.g.| is_integrable_on M ) by A1, MESFUNC5:106;
then A3: |.f.| + |.g.| is_integrable_on M by MESFUNC5:114;
set F = |.f.|;
set G = |.g.|;
A4: f + g is_integrable_on M by A1, MESFUNC5:114;
then ex A being Element of S st
( A = dom (f + g) & f + g is_measurable_on A ) by MESFUNC5:def 17;
then A5: |.(f + g).| is_integrable_on M by A4, MESFUNC5:106;
for x being Element of X st x in dom |.(f + g).| holds
|.(f + g).| . x <= (|.f.| + |.g.|) . x by Th21;
then (|.f.| + |.g.|) - |.(f + g).| is nonnegative by Th1;
then consider E being Element of S such that
A6: ( E = (dom (|.f.| + |.g.|)) /\ (dom |.(f + g).|) & Integral M,(|.(f + g).| | E) <= Integral M,((|.f.| + |.g.|) | E) ) by A3, A5, Th3;
take E ; :: thesis: ( E = dom (f + g) & Integral M,(|.(f + g).| | E) <= (Integral M,(|.f.| | E)) + (Integral M,(|.g.| | E)) )
( |.f.| | E is_integrable_on M & |.g.| | E is_integrable_on M ) by A2, MESFUNC5:103;
then consider E1 being Element of S such that
A7: ( E1 = (dom (|.f.| | E)) /\ (dom (|.g.| | E)) & Integral M,((|.f.| | E) + (|.g.| | E)) = (Integral M,((|.f.| | E) | E1)) + (Integral M,((|.g.| | E) | E1)) ) by MESFUNC5:115;
A8: dom (|.f.| + |.g.|) = (dom f) /\ (dom g) by Th19;
A9: 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 ;
then A10: E = dom |.(f + g).| by A6, A8, XBOOLE_1:28, XBOOLE_1:36;
( dom (|.f.| | E) = (dom |.f.|) /\ E & dom (|.g.| | E) = (dom |.g.|) /\ E ) by RELAT_1:90;
then ( dom (|.f.| | E) = (dom f) /\ E & dom (|.g.| | E) = (dom g) /\ E ) by MESFUNC1:def 10;
then E1 = (((dom f) /\ E) /\ E) /\ (dom g) by A7, 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 E1 = E by A6, A8, A9, XBOOLE_1:28, XBOOLE_1:36;
then ( (|.f.| | E) | E1 = |.f.| | E & (|.g.| | E) | E1 = |.g.| | E ) by FUNCT_1:82;
hence ( E = dom (f + g) & Integral M,(|.(f + g).| | E) <= (Integral M,(|.f.| | E)) + (Integral M,(|.g.| | E)) ) by A6, A7, A10, Th20, MESFUNC1:def 10; :: thesis: verum