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 E1 being Element of S st
( E1 = dom f & f is E1 -measurable ) & ex E2 being Element of S st
( E2 = dom g & g is E2 -measurable ) holds
ex E being Element of S st
( E = dom (f + g) & f + g is E -measurable )
let S be SigmaField of X; for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL st ex E1 being Element of S st
( E1 = dom f & f is E1 -measurable ) & ex E2 being Element of S st
( E2 = dom g & g is E2 -measurable ) holds
ex E being Element of S st
( E = dom (f + g) & f + g is E -measurable )
let M be sigma_Measure of S; for f, g being PartFunc of X,ExtREAL st ex E1 being Element of S st
( E1 = dom f & f is E1 -measurable ) & ex E2 being Element of S st
( E2 = dom g & g is E2 -measurable ) holds
ex E being Element of S st
( E = dom (f + g) & f + g is E -measurable )
let f, g be PartFunc of X,ExtREAL; ( ex E1 being Element of S st
( E1 = dom f & f is E1 -measurable ) & ex E2 being Element of S st
( E2 = dom g & g is E2 -measurable ) implies ex E being Element of S st
( E = dom (f + g) & f + g is E -measurable ) )
assume that
A1:
ex E1 being Element of S st
( E1 = dom f & f is E1 -measurable )
and
A2:
ex E2 being Element of S st
( E2 = dom g & g is E2 -measurable )
; ex E being Element of S st
( E = dom (f + g) & f + g is E -measurable )
consider E1 being Element of S such that
A3:
E1 = dom f
and
A4:
f is E1 -measurable
by A1;
consider E2 being Element of S such that
A5:
E2 = dom g
and
A6:
g is E2 -measurable
by A2;
set E3 = E1 /\ E2;
set g1 = g | (E1 /\ E2);
A7:
(g | (E1 /\ E2)) " {-infty} = (E1 /\ E2) /\ (g " {-infty})
by FUNCT_1:70;
set f1 = f | (E1 /\ E2);
dom (f | (E1 /\ E2)) = (dom f) /\ (E1 /\ E2)
by RELAT_1:61;
then A8:
dom (f | (E1 /\ E2)) = E1 /\ E2
by A3, XBOOLE_1:17, XBOOLE_1:28;
g is E1 /\ E2 -measurable
by A6, MESFUNC1:30, XBOOLE_1:17;
then A9:
g | (E1 /\ E2) is E1 /\ E2 -measurable
by Lm6;
A10:
(g | (E1 /\ E2)) " {+infty} = (E1 /\ E2) /\ (g " {+infty})
by FUNCT_1:70;
dom (g | (E1 /\ E2)) = (dom g) /\ (E1 /\ E2)
by RELAT_1:61;
then A11:
dom (g | (E1 /\ E2)) = E1 /\ E2
by A5, XBOOLE_1:17, XBOOLE_1:28;
(f | (E1 /\ E2)) " {+infty} = (E1 /\ E2) /\ (f " {+infty})
by FUNCT_1:70;
then A12: ((f | (E1 /\ E2)) " {+infty}) /\ ((g | (E1 /\ E2)) " {-infty}) =
(f " {+infty}) /\ ((E1 /\ E2) /\ ((E1 /\ E2) /\ (g " {-infty})))
by A7, XBOOLE_1:16
.=
(f " {+infty}) /\ (((E1 /\ E2) /\ (E1 /\ E2)) /\ (g " {-infty}))
by XBOOLE_1:16
.=
((f " {+infty}) /\ (g " {-infty})) /\ (E1 /\ E2)
by XBOOLE_1:16
;
A13:
dom ((f | (E1 /\ E2)) + (g | (E1 /\ E2))) = ((dom (f | (E1 /\ E2))) /\ (dom (g | (E1 /\ E2)))) \ ((((f | (E1 /\ E2)) " {-infty}) /\ ((g | (E1 /\ E2)) " {+infty})) \/ (((f | (E1 /\ E2)) " {+infty}) /\ ((g | (E1 /\ E2)) " {-infty})))
by MESFUNC1:def 3;
f is E1 /\ E2 -measurable
by A4, MESFUNC1:30, XBOOLE_1:17;
then
f | (E1 /\ E2) is E1 /\ E2 -measurable
by Lm6;
then consider E being Element of S such that
A14:
E = dom ((f | (E1 /\ E2)) + (g | (E1 /\ E2)))
and
A15:
(f | (E1 /\ E2)) + (g | (E1 /\ E2)) is E -measurable
by A9, A8, A11, Lm7;
take
E
; ( E = dom (f + g) & f + g is E -measurable )
A16:
dom ((f + g) | E) = (dom (f + g)) /\ E
by RELAT_1:61;
(f | (E1 /\ E2)) " {-infty} = (E1 /\ E2) /\ (f " {-infty})
by FUNCT_1:70;
then ((f | (E1 /\ E2)) " {-infty}) /\ ((g | (E1 /\ E2)) " {+infty}) =
(f " {-infty}) /\ ((E1 /\ E2) /\ ((E1 /\ E2) /\ (g " {+infty})))
by A10, XBOOLE_1:16
.=
(f " {-infty}) /\ (((E1 /\ E2) /\ (E1 /\ E2)) /\ (g " {+infty}))
by XBOOLE_1:16
.=
((f " {-infty}) /\ (g " {+infty})) /\ (E1 /\ E2)
by XBOOLE_1:16
;
then A17:
(((f | (E1 /\ E2)) " {-infty}) /\ ((g | (E1 /\ E2)) " {+infty})) \/ (((f | (E1 /\ E2)) " {+infty}) /\ ((g | (E1 /\ E2)) " {-infty})) = (E1 /\ E2) /\ (((f " {-infty}) /\ (g " {+infty})) \/ ((f " {+infty}) /\ (g " {-infty})))
by A12, XBOOLE_1:23;
A18:
dom (f + g) = ((dom f) /\ (dom g)) \ (((f " {-infty}) /\ (g " {+infty})) \/ ((f " {+infty}) /\ (g " {-infty})))
by MESFUNC1:def 3;
then A19:
dom (f + g) = E
by A3, A5, A8, A11, A14, A13, A17, XBOOLE_1:47;
now for v being Element of X st v in dom ((f + g) | E) holds
((f + g) | E) . v = ((f | (E1 /\ E2)) + (g | (E1 /\ E2))) . vlet v be
Element of
X;
( v in dom ((f + g) | E) implies ((f + g) | E) . v = ((f | (E1 /\ E2)) + (g | (E1 /\ E2))) . v )assume A20:
v in dom ((f + g) | E)
;
((f + g) | E) . v = ((f | (E1 /\ E2)) + (g | (E1 /\ E2))) . vthen A21:
v in (dom (f + g)) /\ E
by RELAT_1:61;
then A22:
v in dom (f + g)
by XBOOLE_0:def 4;
A23:
((f + g) | E) . v =
(f + g) . v
by A20, FUNCT_1:47
.=
(f . v) + (g . v)
by A22, MESFUNC1:def 3
;
A24:
v in E
by A21, XBOOLE_0:def 4;
A25:
E c= E1 /\ E2
by A8, A11, A14, A13, XBOOLE_1:36;
((f | (E1 /\ E2)) + (g | (E1 /\ E2))) . v =
((f | (E1 /\ E2)) . v) + ((g | (E1 /\ E2)) . v)
by A14, A19, A16, A20, MESFUNC1:def 3
.=
(f . v) + ((g | (E1 /\ E2)) . v)
by A8, A24, A25, FUNCT_1:47
;
hence
((f + g) | E) . v = ((f | (E1 /\ E2)) + (g | (E1 /\ E2))) . v
by A11, A24, A25, A23, FUNCT_1:47;
verum end;
then
(f + g) | E = (f | (E1 /\ E2)) + (g | (E1 /\ E2))
by A14, A19, A16, PARTFUN1:5;
hence
( E = dom (f + g) & f + g is E -measurable )
by A3, A5, A8, A11, A14, A15, A13, A17, A18, Lm6, XBOOLE_1:47; verum