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 st f is_integrable_on M & g is_integrable_on M & dom f = dom g holds
( f + g is_integrable_on M & Integral (M,(f + g)) = (Integral (M,f)) + (Integral (M,g)) )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M & dom f = dom g holds
( f + g is_integrable_on M & Integral (M,(f + g)) = (Integral (M,f)) + (Integral (M,g)) )
let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,ExtREAL st f is_integrable_on M & g is_integrable_on M & dom f = dom g holds
( f + g is_integrable_on M & Integral (M,(f + g)) = (Integral (M,f)) + (Integral (M,g)) )
let f, g be PartFunc of X,ExtREAL; :: thesis: ( f is_integrable_on M & g is_integrable_on M & dom f = dom g implies ( f + g is_integrable_on M & Integral (M,(f + g)) = (Integral (M,f)) + (Integral (M,g)) ) )
assume that
A1: f is_integrable_on M and
A2: g is_integrable_on M and
A3: dom f = dom g ; :: thesis: ( f + g is_integrable_on M & Integral (M,(f + g)) = (Integral (M,f)) + (Integral (M,g)) )
thus f + g is_integrable_on M by A1, A2, Th108; :: thesis: Integral (M,(f + g)) = (Integral (M,f)) + (Integral (M,g))
then A4: ex K0 being Element of S st
( K0 = dom (f + g) & f + g is K0 -measurable ) ;
ex E, NFG, NFPG being Element of S st
( E c= dom f & NFG c= dom f & E = (dom f) \ NFG & f | E is real-valued & E = dom (f | E) & f | E is E -measurable & f | E is_integrable_on M & Integral (M,f) = Integral (M,(f | E)) & E c= dom g & NFG c= dom g & E = (dom g) \ NFG & g | E is real-valued & E = dom (g | E) & g | E is E -measurable & g | E is_integrable_on M & Integral (M,g) = Integral (M,(g | E)) & E c= dom (f + g) & NFPG c= dom (f + g) & E = (dom (f + g)) \ NFPG & M . NFG = 0 & M . NFPG = 0 & E = dom ((f + g) | E) & (f + g) | E is E -measurable & (f + g) | E is_integrable_on M & (f + g) | E = (f | E) + (g | E) & Integral (M,((f + g) | E)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) ) by A1, A2, A3, Lm12;
hence Integral (M,(f + g)) = (Integral (M,f)) + (Integral (M,g)) by A4, Th95; :: thesis: verum