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 nonpositive & f is E1 -measurable & E2 = dom g & g is nonpositive & g is E2 -measurable holds
Integral (M,(f + g)) = (Integral (M,(f | (dom (f + g))))) + (Integral (M,(g | (dom (f + g)))))
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 nonpositive & f is E1 -measurable & E2 = dom g & g is nonpositive & g is E2 -measurable holds
Integral (M,(f + g)) = (Integral (M,(f | (dom (f + g))))) + (Integral (M,(g | (dom (f + g)))))
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 nonpositive & f is E1 -measurable & E2 = dom g & g is nonpositive & g is E2 -measurable holds
Integral (M,(f + g)) = (Integral (M,(f | (dom (f + g))))) + (Integral (M,(g | (dom (f + g)))))
let A, B be Element of S; :: thesis: for f, g being PartFunc of X,ExtREAL st A = dom f & f is nonpositive & f is A -measurable & B = dom g & g is nonpositive & g is B -measurable holds
Integral (M,(f + g)) = (Integral (M,(f | (dom (f + g))))) + (Integral (M,(g | (dom (f + g)))))
let f, g be PartFunc of X,ExtREAL; :: thesis: ( A = dom f & f is nonpositive & f is A -measurable & B = dom g & g is nonpositive & g is B -measurable implies Integral (M,(f + g)) = (Integral (M,(f | (dom (f + g))))) + (Integral (M,(g | (dom (f + g))))) )
assume that
A1: A = dom f and
A2: f is nonpositive and
A3: f is A -measurable and
A4: B = dom g and
A5: g is nonpositive and
A6: g is B -measurable ; :: thesis: Integral (M,(f + g)) = (Integral (M,(f | (dom (f + g))))) + (Integral (M,(g | (dom (f + g)))))
reconsider f1 = - f as nonnegative PartFunc of X,ExtREAL by A2;
reconsider g1 = - g as nonnegative PartFunc of X,ExtREAL by A5;
A7: f1 + g1 = - (f + g) by MEASUR11:64;
then A13: f + g = - (f1 + g1) by MESFUN11:36;
A8: ( dom f1 = A & dom g1 = B ) by A1, A4, MESFUNC1:def 7;
then A9: dom (f1 + g1) = A /\ B by MESFUNC5:22;
then A10: dom (f + g) = A /\ B by A7, MESFUNC1:def 7;
then A11: ( dom (f | (dom (f + g))) = A /\ B & dom (g | (dom (f + g))) = A /\ B ) by A1, A4, XBOOLE_1:17, RELAT_1:62;
A12: ( (dom f) /\ (A /\ B) = A /\ B & (dom g) /\ (A /\ B) = A /\ B ) by A1, A4, XBOOLE_1:17, XBOOLE_1:28;
A14: ( f is A /\ B -measurable & g is A /\ B -measurable ) by A3, A6, XBOOLE_1:17, MESFUNC1:30;
then A15: ( f | (dom (f + g)) is A /\ B -measurable & g | (dom (f + g)) is A /\ B -measurable ) by A10, A12, MESFUNC5:42;
A16: ( f | (dom (f + g)) is nonpositive & g | (dom (f + g)) is nonpositive ) by A2, A5, MESFUN11:1;
( f1 | (dom (f1 + g1)) = - (f | (dom (f + g))) & g1 | (dom (f1 + g1)) = - (g | (dom (f + g))) ) by A9, A10, MESFUN11:3;
then A17: ( Integral (M,(f | (dom (f + g)))) = - (Integral (M,(f1 | (dom (f1 + g1))))) & Integral (M,(g | (dom (f + g)))) = - (Integral (M,(g1 | (dom (f1 + g1))))) ) by A11, A15, A16, MESFUN11:57;
( f + g = (- 1) (#) (f1 + g1) & f1 + g1 is nonnegative ) by A13, MESFUNC2:9, MESFUNC5:19;
then A18: f + g is nonpositive by MESFUNC5:20;
f + g is A /\ B -measurable by A2, A5, A10, A14, MEASUR11:65;
then A19: Integral (M,(f + g)) = - (Integral (M,(f1 + g1))) by A7, A10, A18, MESFUN11:57;
( f1 is A -measurable & g1 is B -measurable ) by A1, A3, A4, A6, MEASUR11:63;
then Integral (M,(f1 + g1)) = (Integral (M,(f1 | (dom (f1 + g1))))) + (Integral (M,(g1 | (dom (f1 + g1))))) by A8, Th21;
hence Integral (M,(f + g)) = (Integral (M,(f | (dom (f + g))))) + (Integral (M,(g | (dom (f + g))))) by A17, A19, XXREAL_3:9; :: thesis: verum