let X be non empty set ; for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for A, B, E being Element of S st E = dom f & f is E -measurable & f is nonpositive & A misses B holds
Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))
let S be SigmaField of X; for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for A, B, E being Element of S st E = dom f & f is E -measurable & f is nonpositive & A misses B holds
Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))
let M be sigma_Measure of S; for f being PartFunc of X,ExtREAL
for A, B, E being Element of S st E = dom f & f is E -measurable & f is nonpositive & A misses B holds
Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))
let f be PartFunc of X,ExtREAL; for A, B, E being Element of S st E = dom f & f is E -measurable & f is nonpositive & A misses B holds
Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))
let A, B, E be Element of S; ( E = dom f & f is E -measurable & f is nonpositive & A misses B implies Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B))) )
assume that
A1:
( E = dom f & f is E -measurable )
and
A2:
f is nonpositive
and
A3:
A misses B
; Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))
set f1 = f | (A \/ B);
set f2 = f | A;
set f3 = f | B;
set g = - f;
reconsider E1 = E /\ (A \/ B) as Element of S ;
A4:
dom (f | (A \/ B)) = E1
by A1, RELAT_1:61;
A5:
E1 = (dom f) /\ E1
by A1, XBOOLE_1:17, XBOOLE_1:28;
A6:
f is E1 -measurable
by A1, XBOOLE_1:17, MESFUNC1:30;
A7:
f | E1 = (f | E) | (A \/ B)
by RELAT_1:71;
(- f) | (A \/ B) = - (f | (A \/ B))
by Th3;
then A8:
Integral (M,((- f) | (A \/ B))) = - (Integral (M,(f | (A \/ B))))
by A1, A4, A5, A6, A7, Th52, MESFUNC5:42;
reconsider E2 = E /\ A as Element of S ;
A9:
dom (f | A) = E2
by A1, RELAT_1:61;
A10:
E2 = (dom f) /\ E2
by A1, XBOOLE_1:17, XBOOLE_1:28;
A11:
f is E2 -measurable
by A1, XBOOLE_1:17, MESFUNC1:30;
A12:
f | E2 = (f | E) | A
by RELAT_1:71;
(- f) | A = - (f | A)
by Th3;
then A13:
Integral (M,((- f) | A)) = - (Integral (M,(f | A)))
by A1, A9, A10, A11, A12, Th52, MESFUNC5:42;
reconsider E3 = E /\ B as Element of S ;
A14:
dom (f | B) = E3
by A1, RELAT_1:61;
A15:
E3 = (dom f) /\ E3
by A1, XBOOLE_1:17, XBOOLE_1:28;
A16:
f is E3 -measurable
by A1, XBOOLE_1:17, MESFUNC1:30;
A17:
f | E3 = (f | E) | B
by RELAT_1:71;
(- f) | B = - (f | B)
by Th3;
then A18:
Integral (M,((- f) | B)) = - (Integral (M,(f | B)))
by A1, A14, A15, A16, A17, Th52, MESFUNC5:42;
E = dom (- f)
by A1, MESFUNC1:def 7;
then
Integral (M,((- f) | (A \/ B))) = (Integral (M,((- f) | A))) + (Integral (M,((- f) | B)))
by A2, A3, A1, MEASUR11:63, MESFUNC5:91;
then
- (Integral (M,(f | (A \/ B)))) = - ((Integral (M,(f | A))) + (Integral (M,(f | B))))
by A8, A13, A18, XXREAL_3:9;
hence
Integral (M,(f | (A \/ B))) = (Integral (M,(f | A))) + (Integral (M,(f | B)))
by XXREAL_3:10; verum