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,ExtREAL st f is_integrable_on M & g is_integrable_on M holds
ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral M,(f + g) = (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,ExtREAL st f is_integrable_on M & g is_integrable_on M holds
ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral M,(f + g) = (Integral M,(f | E)) + (Integral M,(g | E)) )
let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M holds
ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral M,(f + g) = (Integral M,(f | E)) + (Integral M,(g | E)) )
let f, g be PartFunc of X,ExtREAL ; :: thesis: ( f is_integrable_on M & g is_integrable_on M implies ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral M,(f + g) = (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) /\ (dom g) & Integral M,(f + g) = (Integral M,(f | E)) + (Integral M,(g | E)) )
consider B being Element of S such that
A3: B = dom g and
g is_measurable_on B by A2, Def17;
consider A being Element of S such that
A4: A = dom f and
f is_measurable_on A by A1, Def17;
set E = A /\ B;
set g1 = g | (A /\ B);
set f1 = f | (A /\ B);
take E = A /\ B; :: thesis: ( E = (dom f) /\ (dom g) & Integral M,(f + g) = (Integral M,(f | E)) + (Integral M,(g | E)) )
A5: dom (f | (A /\ B)) = (dom f) /\ (A /\ B) by RELAT_1:90
.= (A /\ A) /\ B by A4, XBOOLE_1:16 ;
A6: (f | (A /\ B)) " {+infty } = E /\ (f " {+infty }) by FUNCT_1:139;
(g | (A /\ B)) " {-infty } = E /\ (g " {-infty }) by FUNCT_1:139;
then A7: ((f | (A /\ B)) " {+infty }) /\ ((g | (A /\ B)) " {-infty }) = (((f " {+infty }) /\ E) /\ E) /\ (g " {-infty }) by A6, XBOOLE_1:16
.= ((f " {+infty }) /\ (E /\ E)) /\ (g " {-infty }) by XBOOLE_1:16
.= E /\ ((f " {+infty }) /\ (g " {-infty })) by XBOOLE_1:16 ;
A8: (g | (A /\ B)) " {+infty } = E /\ (g " {+infty }) by FUNCT_1:139;
(f | (A /\ B)) " {-infty } = E /\ (f " {-infty }) by FUNCT_1:139;
then ((f | (A /\ B)) " {-infty }) /\ ((g | (A /\ B)) " {+infty }) = (((f " {-infty }) /\ E) /\ E) /\ (g " {+infty }) by A8, XBOOLE_1:16
.= ((f " {-infty }) /\ (E /\ E)) /\ (g " {+infty }) by XBOOLE_1:16
.= E /\ ((f " {-infty }) /\ (g " {+infty })) by XBOOLE_1:16 ;
then A9: (((f | (A /\ B)) " {-infty }) /\ ((g | (A /\ B)) " {+infty })) \/ (((f | (A /\ B)) " {+infty }) /\ ((g | (A /\ B)) " {-infty })) = E /\ (((f " {-infty }) /\ (g " {+infty })) \/ ((f " {+infty }) /\ (g " {-infty }))) by A7, XBOOLE_1:23;
A10: dom (g | (A /\ B)) = (dom g) /\ (A /\ B) by RELAT_1:90
.= (B /\ B) /\ A by A3, XBOOLE_1:16 ;
A11: dom ((f | (A /\ B)) + (g | (A /\ B))) = ((dom (f | (A /\ B))) /\ (dom (g | (A /\ B)))) \ ((((f | (A /\ B)) " {-infty }) /\ ((g | (A /\ B)) " {+infty })) \/ (((f | (A /\ B)) " {+infty }) /\ ((g | (A /\ B)) " {-infty }))) by MESFUNC1:def 3
.= E \ (((f " {-infty }) /\ (g " {+infty })) \/ ((f " {+infty }) /\ (g " {-infty }))) by A5, A10, A9, XBOOLE_1:47
.= dom (f + g) by A4, A3, MESFUNC1:def 3 ;
A12: for x being set st x in dom ((f | (A /\ B)) + (g | (A /\ B))) holds
((f | (A /\ B)) + (g | (A /\ B))) . x = (f + g) . x

proof

let x be set ; :: thesis: ( x in dom ((f | (A /\ B)) + (g | (A /\ B))) implies ((f | (A /\ B)) + (g | (A /\ B))) . x = (f + g) . x )
assume A13: x in dom ((f | (A /\ B)) + (g | (A /\ B))) ; :: thesis: ((f | (A /\ B)) + (g | (A /\ B))) . x = (f + g) . x
then x in ((dom (f | (A /\ B))) /\ (dom (g | (A /\ B)))) \ ((((f | (A /\ B)) " {-infty }) /\ ((g | (A /\ B)) " {+infty })) \/ (((f | (A /\ B)) " {+infty }) /\ ((g | (A /\ B)) " {-infty }))) by MESFUNC1:def 3;
then A14: x in (dom (f | (A /\ B))) /\ (dom (g | (A /\ B))) by XBOOLE_0:def 5;
then A15: x in dom (f | (A /\ B)) by XBOOLE_0:def 4;
A16: x in dom (g | (A /\ B)) by A14, XBOOLE_0:def 4;
((f | (A /\ B)) + (g | (A /\ B))) . x = ((f | (A /\ B)) . x) + ((g | (A /\ B)) . x) by A13, MESFUNC1:def 3
.= (f . x) + ((g | (A /\ B)) . x) by A15, FUNCT_1:70
.= (f . x) + (g . x) by A16, FUNCT_1:70 ;
hence ((f | (A /\ B)) + (g | (A /\ B))) . x = (f + g) . x by A11, A13, MESFUNC1:def 3; :: thesis: verum

end;

thus E = (dom f) /\ (dom g) by A4, A3; :: thesis: Integral M,(f + g) = (Integral M,(f | E)) + (Integral M,(g | E))
A17: g | (A /\ B) is_integrable_on M by A2, Th103;
f | (A /\ B) is_integrable_on M by A1, Th103;
then Integral M,((f | (A /\ B)) + (g | (A /\ B))) = (Integral M,(f | (A /\ B))) + (Integral M,(g | (A /\ B))) by A17, A5, A10, Lm13;
hence Integral M,(f + g) = (Integral M,(f | E)) + (Integral M,(g | E)) by A11, A12, FUNCT_1:9; :: thesis: verum