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 er being ExtReal holds Integral (M,((chi (er,E1,X)) | E2)) = er * (M . (E1 /\ E2))
let S be SigmaField of X; :: thesis: 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; :: thesis: 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; :: thesis: for er being ExtReal holds Integral (M,((chi (er,E1,X)) | E2)) = er * (M . (E1 /\ E2))
let er be ExtReal; :: thesis: 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; :: thesis: verum