let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let A, B be Element of S; :: thesis:
let f, g be PartFunc of X,ExtREAL; :: thesis:
assume that
A1: A = dom f and
A2: f is nonnegative and
A3: f is A -measurable and
A4: B = dom g and
A5: g is nonnegative and
A6: g is B -measurable ; :: thesis:
set f1 = f | (A /\ B);
set g1 = g | (A /\ B);
A7: dom (f + g) = A /\ B by A1, A2, A4, A5, MESFUNC5:22;
A8: ( dom (f | (A /\ B)) = A /\ B & dom (g | (A /\ B)) = A /\ B & (dom f) /\ (A /\ B) = A /\ B & (dom g) /\ (A /\ B) = A /\ B ) by A1, A4, XBOOLE_1:17, XBOOLE_1:28, RELAT_1:62;
A9: ( f is A /\ B -measurable & g is A /\ B -measurable ) by A3, A6, XBOOLE_1:17, MESFUNC1:30;
A10: f + g is nonnegative by A2, A5, MESFUNC5:22;
( f | (A /\ B) is nonnegative & g | (A /\ B) is nonnegative ) by A2, A5, MESFUNC5:15;
then A11: ( Integral (M,(f | (A /\ B))) = integral+ (M,(f | (A /\ B))) & Integral (M,(g | (A /\ B))) = integral+ (M,(g | (A /\ B))) ) by A8, A9, MESFUNC5:42, MESFUNC5:88;
ex C being Element of S st
( C = dom (f + g) & integral+ (M,(f + g)) = (integral+ (M,(f | C))) + (integral+ (M,(g | C))) ) by A1, A2, A3, A4, A5, A6, MESFUNC5:78;
hence Integral (M,(f + g)) = (Integral (M,(f | (dom (f + g))))) + (Integral (M,(g | (dom (f + g))))) by A2, A5, A7, A9, A10, A11, MESFUNC5:31, MESFUNC5:88; :: thesis: