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 A1: ( f is_integrable_on M & g is_integrable_on M & 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) )
dom (f + g) = ((dom f) /\ (dom g)) \ (((f " {-infty }) /\ (g " {+infty })) \/ ((f " {+infty }) /\ (g " {-infty }))) by MESFUNC1:def 3;
then ( dom (f + g) c= (dom f) /\ (dom g) & (dom f) /\ (dom g) c= dom f & (dom f) /\ (dom g) c= dom g ) by XBOOLE_1:17, XBOOLE_1:36;
then ( dom (f + g) c= dom f & dom (f + g) c= dom g ) by XBOOLE_1:1;
then A2: ( B c= dom f & B c= dom g ) by A1, XBOOLE_1:1;
( dom (f | B) = (dom f) /\ B & dom (g | B) = (dom g) /\ B ) by RELAT_1:90;
then A3: ( f | B is_integrable_on M & dom (f | B) = B & g | B is_integrable_on M & dom (g | B) = B ) by A1, A2, Th103, XBOOLE_1:28;
Integral_on M,B,(f + g) = Integral M,((f | B) + (g | B)) by A1, Th35;
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, A3, Lm14, Th114; :: thesis: verum