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 A1, A2, MESFUNC5:109;
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 A2, MESFUNC5:def 17;
then A4: g is E -measurable by A3, XBOOLE_1:17, MESFUNC1:30;
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 A1, A2, MESFUN10:13;
then Integral (M,(f - g)) = (Integral (M,(f | E))) + (- (Integral (M,(g | E)))) by A3, A4, XBOOLE_1:17, MESFUN11:55;
hence Integral (M,(f - g)) = (Integral (M,(f | ((dom f) /\ (dom g))))) - (Integral (M,(g | ((dom f) /\ (dom g))))) by A3, XXREAL_3:def 4; :: thesis: verum