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 A2, MESFUN6C:def 2;

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 A1, MESFUN6C:def 2;

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 A2, MESFUN6C:def 2;

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 A6, COMSEQ_3:def 3;

f + g is_integrable_on M by A1, A2, MESFUN6C:33;

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 <= (|.f.| + |.g.|) . x by Th40;

then A10: (|.f.| + |.g.|) - |.(f + g).| is nonnegative by Th41;

Re f is_integrable_on M by A1, MESFUN6C:def 2;

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 A11, COMSEQ_3:def 3;

reconsider A = A1 /\ B1 as Element of S ;

Re f is A1 -measurable by A12, MESFUNC6:def 1;

then A14: Re f is A -measurable by MESFUNC6:16, XBOOLE_1:17;

A15: dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def 1;

then A16: dom |.(f + g).| = A by A13, A8, VALUED_1:def 11;

Re g is B1 -measurable by A7, MESFUNC6:def 1;

then A17: Re g is A -measurable by MESFUNC6:16, XBOOLE_1:17;

( B2 = dom g & Im g is B2 -measurable ) by A4, COMSEQ_3:def 4, MESFUNC6:def 1;

then Im g is A -measurable by A8, MESFUNC6:16, XBOOLE_1:17;

then A18: g is A -measurable by A17, MESFUN6C:def 1;

then A19: |.g.| is A -measurable by A8, MESFUN6C:30, XBOOLE_1:17;

( A2 = dom f & Im f is A2 -measurable ) by A5, COMSEQ_3:def 4, MESFUNC6:def 1;

then Im f is A -measurable by A13, MESFUNC6:16, XBOOLE_1:17;

then A20: f is A -measurable by A14, MESFUN6C:def 1;

then |.f.| is A -measurable by A13, MESFUN6C:30, XBOOLE_1:17;

then A21: |.f.| + |.g.| is A -measurable by A19, MESFUNC6:26;

A c= A1 by XBOOLE_1:17;

then A22: A c= dom |.f.| by A13, VALUED_1:def 11;

A c= B1 by XBOOLE_1:17;

then A23: A c= dom |.g.| by A8, VALUED_1:def 11;

A24: dom (|.f.| + |.g.|) = (dom |.f.|) /\ (dom |.g.|) by VALUED_1:def 1;

then A25: (dom |.(f + g).|) /\ (dom (|.f.| + |.g.|)) = A by A22, A23, A16, XBOOLE_1:19, XBOOLE_1:28;

|.(f + g).| is A -measurable by A13, A8, A20, A18, A15, MESFUN6C:11, MESFUN6C:30;

then consider E being Element of S such that

A26: E = (dom (|.f.| + |.g.|)) /\ (dom |.(f + g).|) and

A27: Integral (M,(|.(f + g).| | E)) <= Integral (M,((|.f.| + |.g.|) | E)) by A21, A3, A25, A9, A10, MESFUN6C:42;

A28: dom (|.g.| | E) = E by A23, A25, A26, RELAT_1:62;

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 A13, A8, A15, A24, A22, A23, A16, A26, XBOOLE_1:19, XBOOLE_1:28; :: 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 A1, A2, Th35, MESFUNC6:91;

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 A22, A25, A26, RELAT_1:62;

then ( (|.f.| | E) | E1 = |.f.| | E & (|.g.| | E) | E1 = |.g.| | E ) by A29, A28;

hence Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) by A16, A25, A26, A27, A30, Th39; :: thesis: verum

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 A2, MESFUN6C:def 2;

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 A1, MESFUN6C:def 2;

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 A2, MESFUN6C:def 2;

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 A6, COMSEQ_3:def 3;

f + g is_integrable_on M by A1, A2, MESFUN6C:33;

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 <= (|.f.| + |.g.|) . x by Th40;

then A10: (|.f.| + |.g.|) - |.(f + g).| is nonnegative by Th41;

Re f is_integrable_on M by A1, MESFUN6C:def 2;

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 A11, COMSEQ_3:def 3;

reconsider A = A1 /\ B1 as Element of S ;

Re f is A1 -measurable by A12, MESFUNC6:def 1;

then A14: Re f is A -measurable by MESFUNC6:16, XBOOLE_1:17;

A15: dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def 1;

then A16: dom |.(f + g).| = A by A13, A8, VALUED_1:def 11;

Re g is B1 -measurable by A7, MESFUNC6:def 1;

then A17: Re g is A -measurable by MESFUNC6:16, XBOOLE_1:17;

( B2 = dom g & Im g is B2 -measurable ) by A4, COMSEQ_3:def 4, MESFUNC6:def 1;

then Im g is A -measurable by A8, MESFUNC6:16, XBOOLE_1:17;

then A18: g is A -measurable by A17, MESFUN6C:def 1;

then A19: |.g.| is A -measurable by A8, MESFUN6C:30, XBOOLE_1:17;

( A2 = dom f & Im f is A2 -measurable ) by A5, COMSEQ_3:def 4, MESFUNC6:def 1;

then Im f is A -measurable by A13, MESFUNC6:16, XBOOLE_1:17;

then A20: f is A -measurable by A14, MESFUN6C:def 1;

then |.f.| is A -measurable by A13, MESFUN6C:30, XBOOLE_1:17;

then A21: |.f.| + |.g.| is A -measurable by A19, MESFUNC6:26;

A c= A1 by XBOOLE_1:17;

then A22: A c= dom |.f.| by A13, VALUED_1:def 11;

A c= B1 by XBOOLE_1:17;

then A23: A c= dom |.g.| by A8, VALUED_1:def 11;

A24: dom (|.f.| + |.g.|) = (dom |.f.|) /\ (dom |.g.|) by VALUED_1:def 1;

then A25: (dom |.(f + g).|) /\ (dom (|.f.| + |.g.|)) = A by A22, A23, A16, XBOOLE_1:19, XBOOLE_1:28;

|.(f + g).| is A -measurable by A13, A8, A20, A18, A15, MESFUN6C:11, MESFUN6C:30;

then consider E being Element of S such that

A26: E = (dom (|.f.| + |.g.|)) /\ (dom |.(f + g).|) and

A27: Integral (M,(|.(f + g).| | E)) <= Integral (M,((|.f.| + |.g.|) | E)) by A21, A3, A25, A9, A10, MESFUN6C:42;

A28: dom (|.g.| | E) = E by A23, A25, A26, RELAT_1:62;

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 A13, A8, A15, A24, A22, A23, A16, A26, XBOOLE_1:19, XBOOLE_1:28; :: 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 A1, A2, Th35, MESFUNC6:91;

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 A22, A25, A26, RELAT_1:62;

then ( (|.f.| | E) | E1 = |.f.| | E & (|.g.| | E) | E1 = |.g.| | E ) by A29, A28;

hence Integral (M,(|.(f + g).| | E)) <= (Integral (M,(|.f.| | E))) + (Integral (M,(|.g.| | E))) by A16, A25, A26, A27, A30, Th39; :: thesis: verum