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