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;
then consider B being Element of S such that
A4: B = dom (R_EAL f) and
R_EAL f is B -measurable ;
A5: B = dom |.(R_EAL f).| by A4, MESFUNC1:def 10;
|.(R_EAL f).| is_integrable_on M by A3, MESFUNC5:100;
then A6: ex E being Element of S st
( E = dom |.(R_EAL f).| & |.(R_EAL f).| is E -measurable ) ;
A7: R_EAL g is_integrable_on M by A2;
then consider C being Element of S such that
A8: C = dom (R_EAL g) and
R_EAL g is C -measurable ;
A9: C = dom |.(R_EAL g).| by A8, MESFUNC1:def 10;
consider E being Element of S such that
A10: E = dom ((R_EAL f) + (R_EAL g)) and
A11: Integral (M,(|.((R_EAL f) + (R_EAL g)).| | E)) <= (Integral (M,(|.(R_EAL f).| | E))) + (Integral (M,(|.(R_EAL g).| | E))) by A3, A7, MESFUNC7:22;
dom |.((R_EAL f) + (R_EAL g)).| = E by A10, 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:68;
then A12: Integral (M,(|.((R_EAL f) + (R_EAL g)).| | E)) = Integral (M,|.(f + g).|) by MESFUNC6:1;
|.(R_EAL g).| is_integrable_on M by A7, MESFUNC5:100;
then A13: ex E being Element of S st
( E = dom |.(R_EAL g).| & |.(R_EAL g).| is E -measurable ) ;
A14: 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 A10, 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 A9, A13, MESFUNC5:93;
then Integral (M,(|.(R_EAL g).| | E)) <= Integral (M,|.(R_EAL g).|) by A9, RELAT_1:68;
then A15: Integral (M,(|.(R_EAL g).| | E)) <= Integral (M,|.g.|) by MESFUNC6:1;
E c= dom (R_EAL f) by A14, 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 A5, A6, MESFUNC5:93;
then Integral (M,(|.(R_EAL f).| | E)) <= Integral (M,|.(R_EAL f).|) by A5, RELAT_1:68;
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 A15, XXREAL_3:36;
hence Integral (M,(abs (f + g))) <= (Integral (M,(abs f))) + (Integral (M,(abs g))) by A11, A12, XXREAL_0:2; :: thesis: verum