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,REAL st f is_integrable_on M & g is_integrable_on M holds
Integral M,(abs (f + g)) <= (Integral M,(abs f)) + (Integral M,(abs g))
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds
Integral M,(abs (f + g)) <= (Integral M,(abs f)) + (Integral M,(abs g))
let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,REAL st f is_integrable_on M & g is_integrable_on M holds
Integral M,(abs (f + g)) <= (Integral M,(abs f)) + (Integral M,(abs g))
let f, g be PartFunc of X,REAL ; :: thesis: ( f is_integrable_on M & g is_integrable_on M implies Integral M,(abs (f + g)) <= (Integral M,(abs f)) + (Integral M,(abs g)) )
set f1 = R_EAL f;
set g1 = R_EAL g;
assume ( f is_integrable_on M & g is_integrable_on M ) ; :: thesis: Integral M,(abs (f + g)) <= (Integral M,(abs f)) + (Integral M,(abs g))
then A1: ( R_EAL f is_integrable_on M & R_EAL g is_integrable_on M ) by MESFUNC6:def 9;
then consider E being Element of S such that
A2: ( E = dom ((R_EAL f) + (R_EAL g)) & Integral M,(|.((R_EAL f) + (R_EAL g)).| | E) <= (Integral M,(|.(R_EAL f).| | E)) + (Integral M,(|.(R_EAL g).| | E)) ) by MESFUNC7:22;
consider B being Element of S such that
A3: ( B = dom (R_EAL f) & R_EAL f is_measurable_on B ) by A1, MESFUNC5:def 17;
consider C being Element of S such that
A4: ( C = dom (R_EAL g) & R_EAL g is_measurable_on C ) by A1, MESFUNC5:def 17;
A5: ( B = dom |.(R_EAL f).| & C = dom |.(R_EAL g).| ) by A3, A4, MESFUNC1:def 10;
A7: (R_EAL f) + (R_EAL g) = R_EAL (f + g) by MESFUNC6:23;
dom |.((R_EAL f) + (R_EAL g)).| = E by A2, MESFUNC1:def 10;
then |.((R_EAL f) + (R_EAL g)).| | E = |.((R_EAL f) + (R_EAL g)).| by RELAT_1:97;
then A8: Integral M,(|.((R_EAL f) + (R_EAL g)).| | E) = Integral M,|.(f + g).| by A7, MESFUNC6:1;
E = ((dom (R_EAL f)) /\ (dom (R_EAL g))) \ ((((R_EAL f) " {-infty }) /\ ((R_EAL g) " {+infty })) \/ (((R_EAL f) " {+infty }) /\ ((R_EAL g) " {-infty }))) by A2, MESFUNC1:def 3;
then ( E c= dom (R_EAL f) & E c= dom (R_EAL g) ) by XBOOLE_1:18, XBOOLE_1:36;
then A10: ( E c= dom |.(R_EAL f).| & E c= dom |.(R_EAL g).| ) by MESFUNC1:def 10;
|.(R_EAL f).| is_integrable_on M by A1, A3, MESFUNC5:106;
then ex E being Element of S st
( E = dom |.(R_EAL f).| & |.(R_EAL f).| is_measurable_on E ) by MESFUNC5:def 17;
then Integral M,(|.(R_EAL f).| | E) <= Integral M,(|.(R_EAL f).| | B) by A5, A10, MESFUNC5:99;
then Integral M,(|.(R_EAL f).| | E) <= Integral M,|.(R_EAL f).| by A5, RELAT_1:97;
then A13: Integral M,(|.(R_EAL f).| | E) <= Integral M,|.f.| by MESFUNC6:1;
|.(R_EAL g).| is_integrable_on M by A1, A4, MESFUNC5:106;
then ex E being Element of S st
( E = dom |.(R_EAL g).| & |.(R_EAL g).| is_measurable_on E ) by MESFUNC5:def 17;
then Integral M,(|.(R_EAL g).| | E) <= Integral M,(|.(R_EAL g).| | C) by A5, A10, MESFUNC5:99;
then Integral M,(|.(R_EAL g).| | E) <= Integral M,|.(R_EAL g).| by A5, RELAT_1:97;
then Integral M,(|.(R_EAL g).| | E) <= Integral M,|.g.| by MESFUNC6:1;
then (Integral M,(|.(R_EAL f).| | E)) + (Integral M,(|.(R_EAL g).| | E)) <= (Integral M,|.f.|) + (Integral M,|.g.|) by A13, XXREAL_3:38;
hence Integral M,(abs (f + g)) <= (Integral M,(abs f)) + (Integral M,(abs g)) by A2, A8, XXREAL_0:2; :: thesis: verum