let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let f, g be PartFunc of X,COMPLEX; :: thesis:
assume that
A1: f is_integrable_on M and
A2: g is_integrable_on M ; :: thesis:
( |.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:
thus E = dom (f + g) by A13, A8, A15, A24, A22, A23, A16, A26, XBOOLE_1:19, XBOOLE_1:28; :: thesis:
( |.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: