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 er being ExtReal holds Integral (M,((chi (er,E1,X)) | E2)) = er * (M . (E1 /\ E2))
let S be SigmaField of X; for M being sigma_Measure of S
for E1, E2 being Element of S
for er being ExtReal holds Integral (M,((chi (er,E1,X)) | E2)) = er * (M . (E1 /\ E2))
let M be sigma_Measure of S; for E1, E2 being Element of S
for er being ExtReal holds Integral (M,((chi (er,E1,X)) | E2)) = er * (M . (E1 /\ E2))
let E1, E2 be Element of S; for er being ExtReal holds Integral (M,((chi (er,E1,X)) | E2)) = er * (M . (E1 /\ E2))
let er be ExtReal; Integral (M,((chi (er,E1,X)) | E2)) = er * (M . (E1 /\ E2))
reconsider XX = X as Element of S by MEASURE1:7;
set f = chi (er,(E1 /\ E2),X);
A1:
(chi (er,E1,X)) | E2 = (chi (er,(E1 /\ E2),X)) | E2
by Th14;
A2:
dom (chi (er,(E1 /\ E2),X)) = XX
by FUNCT_2:def 1;
A3:
E1 /\ E2 misses E2 \ E1
by XBOOLE_1:89;
A4:
(E1 /\ E2) \/ (E2 \ E1) = E2
by XBOOLE_1:51;
chi (er,(E1 /\ E2),X) is XX -measurable
by Th13;
then X:
ex W being Element of S st
( W = dom (chi (er,(E1 /\ E2),X)) & chi (er,(E1 /\ E2),X) is W -measurable )
by A2;
( er >= 0 or er < 0 )
;
then
( not chi (er,(E1 /\ E2),X) is V112() or chi (er,(E1 /\ E2),X) is nonpositive )
by Th17;
then A5:
Integral (M,((chi (er,(E1 /\ E2),X)) | E2)) = (Integral (M,((chi (er,(E1 /\ E2),X)) | (E1 /\ E2)))) + (Integral (M,((chi (er,(E1 /\ E2),X)) | (E2 \ E1))))
by X, A3, A4, MESFUNC5:91, MESFUN11:62;
dom ((chi (er,(E1 /\ E2),X)) | (E2 \ E1)) = (dom (chi (er,(E1 /\ E2),X))) /\ (E2 \ E1)
by RELAT_1:61;
then
dom ((chi (er,(E1 /\ E2),X)) | (E2 \ E1)) = X /\ (E2 \ E1)
by FUNCT_2:def 1;
then A6:
dom ((chi (er,(E1 /\ E2),X)) | (E2 \ E1)) = E2 \ E1
by XBOOLE_1:28;
for x being object st x in dom ((chi (er,(E1 /\ E2),X)) | (E2 \ E1)) holds
((chi (er,(E1 /\ E2),X)) | (E2 \ E1)) . x >= 0
by Th16, XBOOLE_1:89;
then A7:
(chi (er,(E1 /\ E2),X)) | (E2 \ E1) is nonnegative
by SUPINF_2:52;
for x being Element of X st x in dom ((chi (er,(E1 /\ E2),X)) | (E2 \ E1)) holds
((chi (er,(E1 /\ E2),X)) | (E2 \ E1)) . x = 0
by Th16, XBOOLE_1:89;
then
integral+ (M,((chi (er,(E1 /\ E2),X)) | (E2 \ E1))) = 0
by A6, Th15, MESFUNC5:87;
then
Integral (M,((chi (er,(E1 /\ E2),X)) | (E2 \ E1))) = 0
by A6, A7, Th15, MESFUNC5:88;
then
Integral (M,((chi (er,(E1 /\ E2),X)) | E2)) = (er * (M . (E1 /\ E2))) + 0
by A5, Th50;
hence
Integral (M,((chi (er,E1,X)) | E2)) = er * (M . (E1 /\ E2))
by A1, XXREAL_3:4; verum