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,ExtREAL st ex E0 being Element of S st
( dom (f + g) = E0 & f + g is E0 -measurable ) & f is_integrable_on M & g is_integrable_on M holds
f + g is_integrable_on M
let S be SigmaField of X; for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL st ex E0 being Element of S st
( dom (f + g) = E0 & f + g is E0 -measurable ) & f is_integrable_on M & g is_integrable_on M holds
f + g is_integrable_on M
let M be sigma_Measure of S; for f, g being PartFunc of X,ExtREAL st ex E0 being Element of S st
( dom (f + g) = E0 & f + g is E0 -measurable ) & f is_integrable_on M & g is_integrable_on M holds
f + g is_integrable_on M
let f, g be PartFunc of X,ExtREAL; ( ex E0 being Element of S st
( dom (f + g) = E0 & f + g is E0 -measurable ) & f is_integrable_on M & g is_integrable_on M implies f + g is_integrable_on M )
assume that
A1:
ex E0 being Element of S st
( dom (f + g) = E0 & f + g is E0 -measurable )
and
A2:
f is_integrable_on M
and
A3:
g is_integrable_on M
; f + g is_integrable_on M
consider E being Element of S such that
A4:
dom (f + g) = E
and
A5:
f + g is E -measurable
by A1;
A6:
|.f.| | E is nonnegative
by Lm1, Th15;
|.g.| is_integrable_on M
by A3, Th100;
then A7:
|.g.| | E is_integrable_on M
by Th97;
A8:
|.g.| | E is nonnegative
by Lm1, Th15;
A9:
dom (f + g) = ((dom f) /\ (dom g)) \ (((f " {-infty}) /\ (g " {+infty})) \/ ((f " {+infty}) /\ (g " {-infty})))
by MESFUNC1:def 3;
then
dom (f + g) c= dom g
by XBOOLE_1:18, XBOOLE_1:36;
then A10:
E c= dom |.g.|
by A4, MESFUNC1:def 10;
then A11:
(dom |.g.|) /\ E = E
by XBOOLE_1:28;
dom (f + g) c= dom f
by A9, XBOOLE_1:18, XBOOLE_1:36;
then A12:
E c= dom |.f.|
by A4, MESFUNC1:def 10;
then
(dom |.f.|) /\ E = E
by XBOOLE_1:28;
then A13:
E = dom (|.f.| | E)
by RELAT_1:61;
then A14:
(dom (|.f.| | E)) /\ (dom (|.g.| | E)) = E /\ E
by A11, RELAT_1:61;
then A15:
dom ((|.f.| | E) + (|.g.| | E)) = E
by A6, A8, Th22;
A16:
E = dom (|.g.| | E)
by A11, RELAT_1:61;
A17:
now for x being Element of X st x in dom (f + g) holds
|.((f + g) . x).| <= ((|.f.| | E) + (|.g.| | E)) . xlet x be
Element of
X;
( x in dom (f + g) implies |.((f + g) . x).| <= ((|.f.| | E) + (|.g.| | E)) . x )A18:
|.((f . x) + (g . x)).| <= |.(f . x).| + |.(g . x).|
by EXTREAL1:24;
assume A19:
x in dom (f + g)
;
|.((f + g) . x).| <= ((|.f.| | E) + (|.g.| | E)) . xthen A20:
x in dom ((|.f.| | E) + (|.g.| | E))
by A4, A6, A8, A14, Th22;
|.(f . x).| + |.(g . x).| =
(|.f.| . x) + |.(g . x).|
by A4, A12, A19, MESFUNC1:def 10
.=
(|.f.| . x) + (|.g.| . x)
by A4, A10, A19, MESFUNC1:def 10
.=
((|.f.| | E) . x) + (|.g.| . x)
by A4, A13, A19, FUNCT_1:47
.=
((|.f.| | E) . x) + ((|.g.| | E) . x)
by A4, A16, A19, FUNCT_1:47
.=
((|.f.| | E) + (|.g.| | E)) . x
by A20, MESFUNC1:def 3
;
hence
|.((f + g) . x).| <= ((|.f.| | E) + (|.g.| | E)) . x
by A19, A18, MESFUNC1:def 3;
verum end;
|.f.| is_integrable_on M
by A2, Th100;
then
|.f.| | E is_integrable_on M
by Th97;
then
(|.f.| | E) + (|.g.| | E) is_integrable_on M
by A7, A6, A8, Th106;
hence
f + g is_integrable_on M
by A4, A5, A17, A15, Th102; verum