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 A1: ( f is_integrable_on M & g is_integrable_on M & dom f = dom g ) ; :: thesis: ( f + g is_integrable_on M & Integral M,(f + g) = (Integral M,f) + (Integral M,g) )
hence A2: f + g is_integrable_on M by Th114; :: thesis: Integral M,(f + g) = (Integral M,f) + (Integral M,g)
A3: 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_measurable_on E & 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_measurable_on E & 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_measurable_on E & (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, Lm13;
ex K0 being Element of S st
( K0 = dom (f + g) & f + g is_measurable_on K0 ) by A2, Def17;
hence Integral M,(f + g) = (Integral M,f) + (Integral M,g) by A3, Th101; :: thesis: verum