let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for E1, E2 being Element of S
for f, g being PartFunc of X,ExtREAL st E1 = dom f & f is nonnegative & f is_measurable_on E1 & E2 = dom g & g is nonpositive & g is_measurable_on E2 holds
( Integral (M,(f - g)) = (Integral (M,(f | (dom (f - g))))) - (Integral (M,(g | (dom (f - g))))) & Integral (M,(g - f)) = (Integral (M,(g | (dom (g - f))))) - (Integral (M,(f | (dom (g - f))))) )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for E1, E2 being Element of S
for f, g being PartFunc of X,ExtREAL st E1 = dom f & f is nonnegative & f is_measurable_on E1 & E2 = dom g & g is nonpositive & g is_measurable_on E2 holds
( Integral (M,(f - g)) = (Integral (M,(f | (dom (f - g))))) - (Integral (M,(g | (dom (f - g))))) & Integral (M,(g - f)) = (Integral (M,(g | (dom (g - f))))) - (Integral (M,(f | (dom (g - f))))) )
let M be sigma_Measure of S; :: thesis: for E1, E2 being Element of S
for f, g being PartFunc of X,ExtREAL st E1 = dom f & f is nonnegative & f is_measurable_on E1 & E2 = dom g & g is nonpositive & g is_measurable_on E2 holds
( Integral (M,(f - g)) = (Integral (M,(f | (dom (f - g))))) - (Integral (M,(g | (dom (f - g))))) & Integral (M,(g - f)) = (Integral (M,(g | (dom (g - f))))) - (Integral (M,(f | (dom (g - f))))) )
let A, B be Element of S; :: thesis: for f, g being PartFunc of X,ExtREAL st A = dom f & f is nonnegative & f is_measurable_on A & B = dom g & g is nonpositive & g is_measurable_on B holds
( Integral (M,(f - g)) = (Integral (M,(f | (dom (f - g))))) - (Integral (M,(g | (dom (f - g))))) & Integral (M,(g - f)) = (Integral (M,(g | (dom (g - f))))) - (Integral (M,(f | (dom (g - f))))) )
let f, g be PartFunc of X,ExtREAL; :: thesis: ( A = dom f & f is nonnegative & f is_measurable_on A & B = dom g & g is nonpositive & g is_measurable_on B implies ( Integral (M,(f - g)) = (Integral (M,(f | (dom (f - g))))) - (Integral (M,(g | (dom (f - g))))) & Integral (M,(g - f)) = (Integral (M,(g | (dom (g - f))))) - (Integral (M,(f | (dom (g - f))))) ) )
assume that
A1: A = dom f and
A2: f is nonnegative and
A3: f is_measurable_on A and
A4: B = dom g and
A5: g is nonpositive and
A6: g is_measurable_on B ; :: thesis: ( Integral (M,(f - g)) = (Integral (M,(f | (dom (f - g))))) - (Integral (M,(g | (dom (f - g))))) & Integral (M,(g - f)) = (Integral (M,(g | (dom (g - f))))) - (Integral (M,(f | (dom (g - f))))) )
reconsider g1 = - g as nonnegative PartFunc of X,ExtREAL by A5;
A7: B = dom g1 by A4, MESFUNC1:def 7;
A8: g1 is_measurable_on B by A4, A6, MEASUR11:63;
A9: ( f is_measurable_on A /\ B & g is_measurable_on A /\ B ) by A3, A6, XBOOLE_1:17, MESFUNC1:30;
A10: dom (f - g) = A /\ B by A1, A2, A4, A5, MESFUNC5:17;
then A11: A /\ B = dom (g | (dom (f - g))) by A4, XBOOLE_1:17, RELAT_1:62;
then A /\ B = (dom g) /\ (dom (f - g)) by RELAT_1:61;
then A12: g | (dom (f - g)) is_measurable_on A /\ B by A9, A10, MESFUNC5:42;
f + g1 = f - g by MESFUNC2:8;
then A14: Integral (M,(f - g)) = (Integral (M,(f | (dom (f - g))))) + (Integral (M,(g1 | (dom (f - g))))) by A1, A2, A3, A7, A8, Th21;
A15: g | (dom (f - g)) is nonpositive by A5, MESFUN11:1;
g1 | (dom (f - g)) = - (g | (dom (f - g))) by MESFUN11:3;
then Integral (M,(g | (dom (f - g)))) = - (Integral (M,(g1 | (dom (f - g))))) by A12, A11, A15, MESFUN11:57;
then - (Integral (M,(g | (dom (f - g))))) = Integral (M,(g1 | (dom (f - g)))) ;
hence A20: Integral (M,(f - g)) = (Integral (M,(f | (dom (f - g))))) - (Integral (M,(g | (dom (f - g))))) by A14, XXREAL_3:def 4; :: thesis: Integral (M,(g - f)) = (Integral (M,(g | (dom (g - f))))) - (Integral (M,(f | (dom (g - f)))))
A16: g - f = - (f - g) by MEASUR11:64;
then A17: dom (g - f) = A /\ B by A10, MESFUNC1:def 7;
Integral (M,(g - f)) = - (Integral (M,(f - g))) by A2, A5, A9, A10, A16, MESFUN11:52, MEASUR11:67;
hence Integral (M,(g - f)) = (Integral (M,(g | (dom (g - f))))) - (Integral (M,(f | (dom (g - f))))) by A20, A17, A10, XXREAL_3:26; :: thesis: verum