let X be non empty set ; 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 E1 -measurable & E2 = dom g & g is nonnegative & 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; 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 E1 -measurable & E2 = dom g & g is nonnegative & 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; for E1, E2 being Element of S
for f, g being PartFunc of X,ExtREAL st E1 = dom f & f is nonnegative & f is E1 -measurable & E2 = dom g & g is nonnegative & 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; for f, g being PartFunc of X,ExtREAL st A = dom f & f is nonnegative & f is A -measurable & B = dom g & g is nonnegative & 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; ( A = dom f & f is nonnegative & f is A -measurable & B = dom g & g is nonnegative & 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 nonnegative
and
A3:
f is A -measurable
and
A4:
B = dom g
and
A5:
g is nonnegative
and
A6:
g is B -measurable
; Integral (M,(f + g)) = (Integral (M,(f | (dom (f + g))))) + (Integral (M,(g | (dom (f + g)))))
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; verum