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,COMPLEX 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,COMPLEX 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,COMPLEX 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,COMPLEX; :: 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))) )

( |.f.| is_integrable_on M & |.g.| is_integrable_on M ) by A1, A2, Th35;
then A3: |.f.| + |.g.| is_integrable_on M by MESFUNC6:100;
Im g is_integrable_on M by ;
then R_EAL (Im g) is_integrable_on M by MESFUNC6:def 4;
then consider B2 being Element of S such that
A4: ( B2 = dom (R_EAL (Im g)) & R_EAL (Im g) is B2 -measurable ) ;
Im f is_integrable_on M by ;
then R_EAL (Im f) is_integrable_on M by MESFUNC6:def 4;
then consider A2 being Element of S such that
A5: ( A2 = dom (R_EAL (Im f)) & R_EAL (Im f) is A2 -measurable ) ;
Re g is_integrable_on M by ;
then R_EAL (Re g) is_integrable_on M by MESFUNC6:def 4;
then consider B1 being Element of S such that
A6: B1 = dom (R_EAL (Re g)) and
A7: R_EAL (Re g) is B1 -measurable ;
A8: B1 = dom g by ;
f + g is_integrable_on M by ;
then A9: |.(f + g).| is_integrable_on M by Th35;
set G = |.g.|;
set F = |.f.|;
for x being set st x in dom |.(f + g).| holds
|.(f + g).| . x <= () . x by Th40;
then A10: (|.f.| + |.g.|) - |.(f + g).| is nonnegative by Th41;
Re f is_integrable_on M by ;
then R_EAL (Re f) is_integrable_on M by MESFUNC6:def 4;
then consider A1 being Element of S such that
A11: A1 = dom (R_EAL (Re f)) and
A12: R_EAL (Re f) is A1 -measurable ;
A13: A1 = dom f by ;
reconsider A = A1 /\ B1 as Element of S ;
Re f is A1 -measurable by ;
then A14: Re f is A -measurable by ;
A15: dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def 1;
then A16: dom |.(f + g).| = A by ;
Re g is B1 -measurable by ;
then A17: Re g is A -measurable by ;
( B2 = dom g & Im g is B2 -measurable ) by ;
then Im g is A -measurable by ;
then A18: g is A -measurable by ;
then A19: |.g.| is A -measurable by ;
( A2 = dom f & Im f is A2 -measurable ) by ;
then Im f is A -measurable by ;
then A20: f is A -measurable by ;
then |.f.| is A -measurable by ;
then A21: |.f.| + |.g.| is A -measurable by ;
A c= A1 by XBOOLE_1:17;
then A22: A c= dom |.f.| by ;
A c= B1 by XBOOLE_1:17;
then A23: A c= dom |.g.| by ;
A24: dom () = () /\ () by VALUED_1:def 1;
then A25: (dom |.(f + g).|) /\ (dom ()) = A by ;
|.(f + g).| is A -measurable by ;
then consider E being Element of S such that
A26: E = (dom ()) /\ (dom |.(f + g).|) and
A27: Integral (M,(|.(f + g).| | E)) <= Integral (M,(() | E)) by ;
A28: dom (|.g.| | E) = E by ;
take E ; :: thesis: ( E = dom (f + g) & Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) )
thus E = dom (f + g) by ; :: thesis: 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 ;
then consider E1 being Element of S such that
A29: E1 = (dom (|.f.| | E)) /\ (dom (|.g.| | E)) and
A30: Integral (M,((|.f.| | E) + (|.g.| | E))) = (Integral (M,((|.f.| | E) | E1))) + (Integral (M,((|.g.| | E) | E1))) by MESFUNC6:101;
dom (|.f.| | E) = E by ;
then ( (|.f.| | E) | E1 = |.f.| | E & (|.g.| | E) | E1 = |.g.| | E ) by ;
hence Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) by A16, A25, A26, A27, A30, Th39; :: thesis: verum