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
for B being Element of S st f is_integrable_on M & g is_integrable_on M & B c= dom (f + g) holds
( f + g is_integrable_on M & Integral_on (M,B,(f + g)) = (Integral_on (M,B,f)) + (Integral_on (M,B,g)) )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL
for B being Element of S st f is_integrable_on M & g is_integrable_on M & B c= dom (f + g) holds
( f + g is_integrable_on M & Integral_on (M,B,(f + g)) = (Integral_on (M,B,f)) + (Integral_on (M,B,g)) )
let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,ExtREAL
for B being Element of S st f is_integrable_on M & g is_integrable_on M & B c= dom (f + g) holds
( f + g is_integrable_on M & Integral_on (M,B,(f + g)) = (Integral_on (M,B,f)) + (Integral_on (M,B,g)) )
let f, g be PartFunc of X,ExtREAL; :: thesis: for B being Element of S st f is_integrable_on M & g is_integrable_on M & B c= dom (f + g) holds
( f + g is_integrable_on M & Integral_on (M,B,(f + g)) = (Integral_on (M,B,f)) + (Integral_on (M,B,g)) )
let B be Element of S; :: thesis: ( f is_integrable_on M & g is_integrable_on M & B c= dom (f + g) implies ( f + g is_integrable_on M & Integral_on (M,B,(f + g)) = (Integral_on (M,B,f)) + (Integral_on (M,B,g)) ) )
assume that
A1: f is_integrable_on M and
A2: g is_integrable_on M and
A3: B c= dom (f + g) ; :: thesis: ( f + g is_integrable_on M & Integral_on (M,B,(f + g)) = (Integral_on (M,B,f)) + (Integral_on (M,B,g)) )
A4: dom (f | B) = (dom f) /\ B by RELAT_1:61;
dom (f + g) = ((dom f) /\ (dom g)) \ (((f " {-infty}) /\ (g " {+infty})) \/ ((f " {+infty}) /\ (g " {-infty}))) by MESFUNC1:def 3;
then A5: dom (f + g) c= (dom f) /\ (dom g) by XBOOLE_1:36;
(dom f) /\ (dom g) c= dom f by XBOOLE_1:17;
then dom (f + g) c= dom f by A5;
then A6: dom (f | B) = B by A3, A4, XBOOLE_1:1, XBOOLE_1:28;
A7: Integral_on (M,B,(f + g)) = Integral (M,((f | B) + (g | B))) by A3, Th29;
A8: g | B is_integrable_on M by A2, Th97;
A9: dom (g | B) = (dom g) /\ B by RELAT_1:61;
(dom f) /\ (dom g) c= dom g by XBOOLE_1:17;
then dom (f + g) c= dom g by A5;
then A10: dom (g | B) = B by A3, A9, XBOOLE_1:1, XBOOLE_1:28;
f | B is_integrable_on M by A1, Th97;
hence ( f + g is_integrable_on M & Integral_on (M,B,(f + g)) = (Integral_on (M,B,f)) + (Integral_on (M,B,g)) ) by A1, A2, A6, A8, A10, A7, Lm13, Th108; :: thesis: verum