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 A1: ( f is_integrable_on M & 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)) )
then consider A being Element of S such that
A2: ( A = dom f & f is_measurable_on A ) by Def17;
consider B being Element of S such that
A3: ( B = dom g & g is_measurable_on B ) by A1, Def17;
set E = A /\ B;
set f1 = f | (A /\ B);
set g1 = g | (A /\ B);
A4: ( f | (A /\ B) is_integrable_on M & g | (A /\ B) is_integrable_on M ) by A1, Th103;
A5: dom (f | (A /\ B)) = (dom f) /\ (A /\ B) by RELAT_1:90
.= (A /\ A) /\ B by A2, XBOOLE_1:16 ;
A6: dom (g | (A /\ B)) = (dom g) /\ (A /\ B) by RELAT_1:90
.= (B /\ B) /\ A by A3, XBOOLE_1:16 ;
then A7: Integral M,((f | (A /\ B)) + (g | (A /\ B))) = (Integral M,(f | (A /\ B))) + (Integral M,(g | (A /\ B))) by A4, A5, Lm14;
take E = A /\ B; :: thesis: ( E = (dom f) /\ (dom g) & Integral M,(f + g) = (Integral M,(f | E)) + (Integral M,(g | E)) )
thus E = (dom f) /\ (dom g) by A2, A3; :: thesis: Integral M,(f + g) = (Integral M,(f | E)) + (Integral M,(g | E))
A8: ( (f | (A /\ B)) " {-infty } = E /\ (f " {-infty }) & (g | (A /\ B)) " {-infty } = E /\ (g " {-infty }) & (f | (A /\ B)) " {+infty } = E /\ (f " {+infty }) & (g | (A /\ B)) " {+infty } = E /\ (g " {+infty }) ) by FUNCT_1:139;
then A9: ((f | (A /\ B)) " {-infty }) /\ ((g | (A /\ B)) " {+infty }) = (((f " {-infty }) /\ E) /\ E) /\ (g " {+infty }) by XBOOLE_1:16
.= ((f " {-infty }) /\ (E /\ E)) /\ (g " {+infty }) by XBOOLE_1:16
.= E /\ ((f " {-infty }) /\ (g " {+infty })) by XBOOLE_1:16 ;
((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 A10: (((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 A9, XBOOLE_1:23;
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, A6, A10, XBOOLE_1:47
.= dom (f + g) by A2, A3, MESFUNC1:def 3 ;
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 A12: 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 x in (dom (f | (A /\ B))) /\ (dom (g | (A /\ B))) by XBOOLE_0:def 5;
then A13: ( x in dom (f | (A /\ B)) & x in dom (g | (A /\ B)) ) by XBOOLE_0:def 4;
((f | (A /\ B)) + (g | (A /\ B))) . x = ((f | (A /\ B)) . x) + ((g | (A /\ B)) . x) by A12, MESFUNC1:def 3
.= (f . x) + ((g | (A /\ B)) . x) by A13, FUNCT_1:70
.= (f . x) + (g . x) by A13, FUNCT_1:70 ;
hence ((f | (A /\ B)) + (g | (A /\ B))) . x = (f + g) . x by A11, A12, MESFUNC1:def 3; :: thesis: verum

end;

hence Integral M,(f + g) = (Integral M,(f | E)) + (Integral M,(g | E)) by A7, A11, FUNCT_1:9; :: thesis: verum