let X be non empty set ; 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; 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; 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; ( 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
; 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
; ( 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; 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; verum