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:90;
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, XBOOLE_1:1;
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, Th35;
A8: g | B is_integrable_on M by A2, Th103;
A9: dom (g | B) = (dom g) /\ B by RELAT_1:90;
(dom f) /\ (dom g) c= dom g by XBOOLE_1:17;
then dom (f + g) c= dom g by A5, XBOOLE_1:1;
then A10: dom (g | B) = B by A3, A9, XBOOLE_1:1, XBOOLE_1:28;
f | B is_integrable_on M by A1, Th103;
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, Th114; :: thesis: verum