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,REAL
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,REAL
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,REAL
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,REAL; :: 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 & g is_integrable_on M ) and
A2: 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)) )
A3: dom (f + g) = dom (R_EAL (f + g))
.= dom ((R_EAL f) + (R_EAL g)) by Th23 ;
A4: ( R_EAL f is_integrable_on M & R_EAL g is_integrable_on M ) by A1;
then (R_EAL f) + (R_EAL g) is_integrable_on M by A2, A3, MESFUNC5:111;
then A5: R_EAL (f + g) is_integrable_on M by Th23;
Integral_on (M,B,((R_EAL f) + (R_EAL g))) = (Integral_on (M,B,(R_EAL f))) + (Integral_on (M,B,(R_EAL g))) by A2, A4, A3, MESFUNC5:111;
hence ( f + g is_integrable_on M & Integral_on (M,B,(f + g)) = (Integral_on (M,B,f)) + (Integral_on (M,B,g)) ) by A5, Th23; :: thesis: verum