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 that
A1: f is_integrable_on M and
A2: g is_integrable_on M ; :: thesis: Integral (M,(abs (f + g))) <= (Integral (M,(abs f))) + (Integral (M,(abs g)))
A3: R_EAL f is_integrable_on M by A1, MESFUNC6:def 9;
then consider B being Element of S such that
A4: B = dom (R_EAL f) and
A5: R_EAL f is_measurable_on B by MESFUNC5:def 17;
A6: B = dom |.(R_EAL f).| by A4, MESFUNC1:def 10;
|.(R_EAL f).| is_integrable_on M by A3, A4, A5, MESFUNC5:106;
then A7: ex E being Element of S st
( E = dom |.(R_EAL f).| & |.(R_EAL f).| is_measurable_on E ) by MESFUNC5:def 17;
A8: R_EAL g is_integrable_on M by A2, MESFUNC6:def 9;
then consider C being Element of S such that
A9: C = dom (R_EAL g) and
A10: R_EAL g is_measurable_on C by MESFUNC5:def 17;
A11: C = dom |.(R_EAL g).| by A9, MESFUNC1:def 10;
consider E being Element of S such that
A12: E = dom ((R_EAL f) + (R_EAL g)) and
A13: Integral (M,(|.((R_EAL f) + (R_EAL g)).| | E)) <= (Integral (M,(|.(R_EAL f).| | E))) + (Integral (M,(|.(R_EAL g).| | E))) by A3, A8, MESFUNC7:22;
dom |.((R_EAL f) + (R_EAL g)).| = E by A12, MESFUNC1:def 10;
then ( (R_EAL f) + (R_EAL g) = R_EAL (f + g) & |.((R_EAL f) + (R_EAL g)).| | E = |.((R_EAL f) + (R_EAL g)).| ) by MESFUNC6:23, RELAT_1:97;
then A14: Integral (M,(|.((R_EAL f) + (R_EAL g)).| | E)) = Integral (M,|.(f + g).|) by MESFUNC6:1;
|.(R_EAL g).| is_integrable_on M by A8, A9, A10, MESFUNC5:106;
then A15: ex E being Element of S st
( E = dom |.(R_EAL g).| & |.(R_EAL g).| is_measurable_on E ) by MESFUNC5:def 17;
A16: 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 A12, MESFUNC1:def 3;
then E c= dom (R_EAL g) by XBOOLE_1:18, XBOOLE_1:36;
then E c= dom |.(R_EAL g).| by MESFUNC1:def 10;
then Integral (M,(|.(R_EAL g).| | E)) <= Integral (M,(|.(R_EAL g).| | C)) by A11, A15, MESFUNC5:99;
then Integral (M,(|.(R_EAL g).| | E)) <= Integral (M,|.(R_EAL g).|) by A11, RELAT_1:97;
then A17: Integral (M,(|.(R_EAL g).| | E)) <= Integral (M,|.g.|) by MESFUNC6:1;
E c= dom (R_EAL f) by A16, XBOOLE_1:18, XBOOLE_1:36;
then E c= dom |.(R_EAL f).| by MESFUNC1:def 10;
then Integral (M,(|.(R_EAL f).| | E)) <= Integral (M,(|.(R_EAL f).| | B)) by A6, A7, MESFUNC5:99;
then Integral (M,(|.(R_EAL f).| | E)) <= Integral (M,|.(R_EAL f).|) by A6, RELAT_1:97;
then Integral (M,(|.(R_EAL f).| | E)) <= Integral (M,|.f.|) by MESFUNC6:1;
then (Integral (M,(|.(R_EAL f).| | E))) + (Integral (M,(|.(R_EAL g).| | E))) <= (Integral (M,|.f.|)) + (Integral (M,|.g.|)) by A17, XXREAL_3:38;
hence Integral (M,(abs (f + g))) <= (Integral (M,(abs f))) + (Integral (M,(abs g))) by A13, A14, XXREAL_0:2; :: thesis: verum