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 holds
( Integral (M,(f + g)) = (Integral (M,(f | ((dom f) /\ (dom g))))) + (Integral (M,(g | ((dom f) /\ (dom g))))) & Integral (M,(f - g)) = (Integral (M,(f | ((dom f) /\ (dom g))))) - (Integral (M,(g | ((dom f) /\ (dom 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 holds
( Integral (M,(f + g)) = (Integral (M,(f | ((dom f) /\ (dom g))))) + (Integral (M,(g | ((dom f) /\ (dom g))))) & Integral (M,(f - g)) = (Integral (M,(f | ((dom f) /\ (dom g))))) - (Integral (M,(g | ((dom f) /\ (dom 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 holds
( Integral (M,(f + g)) = (Integral (M,(f | ((dom f) /\ (dom g))))) + (Integral (M,(g | ((dom f) /\ (dom g))))) & Integral (M,(f - g)) = (Integral (M,(f | ((dom f) /\ (dom g))))) - (Integral (M,(g | ((dom f) /\ (dom g))))) )

let f, g be PartFunc of X,ExtREAL; :: thesis: ( f is_integrable_on M & g is_integrable_on M implies ( Integral (M,(f + g)) = (Integral (M,(f | ((dom f) /\ (dom g))))) + (Integral (M,(g | ((dom f) /\ (dom g))))) & Integral (M,(f - g)) = (Integral (M,(f | ((dom f) /\ (dom g))))) - (Integral (M,(g | ((dom f) /\ (dom g))))) ) )
assume that
A1: f is_integrable_on M and
A2: g is_integrable_on M ; :: thesis: ( Integral (M,(f + g)) = (Integral (M,(f | ((dom f) /\ (dom g))))) + (Integral (M,(g | ((dom f) /\ (dom g))))) & Integral (M,(f - g)) = (Integral (M,(f | ((dom f) /\ (dom g))))) - (Integral (M,(g | ((dom f) /\ (dom g))))) )
consider E being Element of S such that
A3: ( E = (dom f) /\ (dom g) & Integral (M,(f + g)) = (Integral (M,(f | E))) + (Integral (M,(g | E))) ) by ;
thus Integral (M,(f + g)) = (Integral (M,(f | ((dom f) /\ (dom g))))) + (Integral (M,(g | ((dom f) /\ (dom g))))) by A3; :: thesis: Integral (M,(f - g)) = (Integral (M,(f | ((dom f) /\ (dom g))))) - (Integral (M,(g | ((dom f) /\ (dom g)))))
ex E0 being Element of S st
( E0 = dom g & g is E0 -measurable ) by ;
then A4: g is E -measurable by ;
ex E being Element of S st
( E = (dom f) /\ (dom g) & Integral (M,(f - g)) = (Integral (M,(f | E))) + (Integral (M,((- g) | E))) ) by ;
then Integral (M,(f - g)) = (Integral (M,(f | E))) + (- (Integral (M,(g | E)))) by ;
hence Integral (M,(f - g)) = (Integral (M,(f | ((dom f) /\ (dom g))))) - (Integral (M,(g | ((dom f) /\ (dom g))))) by ; :: thesis: verum