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 B -measurable by A2;
consider A being Element of S such that
A4: A = dom f and
f is A -measurable by A1;
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:61
.= (A /\ A) /\ B by A4, XBOOLE_1:16 ;
A6: (f | (A /\ B)) " {+infty} = E /\ (f " {+infty}) by FUNCT_1:70;
(g | (A /\ B)) " {-infty} = E /\ (g " {-infty}) by FUNCT_1:70;
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:70;
(f | (A /\ B)) " {-infty} = E /\ (f " {-infty}) by FUNCT_1:70;
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:61
.= (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 object 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 object ; :: 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:47
.= (f . x) + (g . x) by A16, FUNCT_1:47 ;
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, Th97;
f | (A /\ B) is_integrable_on M by A1, Th97;
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:2; :: thesis: verum