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 st M . (E1 /\ E2) < +infty holds
Integral (M,((chi (E1,X)) | E2)) = M . (E1 /\ E2)
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for E1, E2 being Element of S st M . (E1 /\ E2) < +infty holds
Integral (M,((chi (E1,X)) | E2)) = M . (E1 /\ E2)
let M be sigma_Measure of S; :: thesis: for E1, E2 being Element of S st M . (E1 /\ E2) < +infty holds
Integral (M,((chi (E1,X)) | E2)) = M . (E1 /\ E2)
let E1, E2 be Element of S; :: thesis: ( M . (E1 /\ E2) < +infty implies Integral (M,((chi (E1,X)) | E2)) = M . (E1 /\ E2) )
reconsider XX = X as Element of S by MEASURE1:7;
A1: E2 = (E1 /\ E2) \/ (E2 \ E1) by XBOOLE_1:51;
set F = E2 \ E1;
A2: dom ((chi (E1,X)) | (E1 /\ E2)) = (dom (chi (E1,X))) /\ (E1 /\ E2) by RELAT_1:61
.= X /\ (E1 /\ E2) by FUNCT_3:def 3 ;
A3: dom ((chi ((E1 /\ E2),X)) | (E1 /\ E2)) = (dom (chi ((E1 /\ E2),X))) /\ (E1 /\ E2) by RELAT_1:61
.= X /\ (E1 /\ E2) by FUNCT_3:def 3 ;
now :: thesis: for x being Element of X st x in dom ((chi (E1,X)) | (E1 /\ E2)) holds
((chi (E1,X)) | (E1 /\ E2)) . x = ((chi ((E1 /\ E2),X)) | (E1 /\ E2)) . x
let x be Element of X; :: thesis: ( x in dom ((chi (E1,X)) | (E1 /\ E2)) implies ((chi (E1,X)) | (E1 /\ E2)) . x = ((chi ((E1 /\ E2),X)) | (E1 /\ E2)) . x )
assume A4: x in dom ((chi (E1,X)) | (E1 /\ E2)) ; :: thesis: ((chi (E1,X)) | (E1 /\ E2)) . x = ((chi ((E1 /\ E2),X)) | (E1 /\ E2)) . x
then A5: ((chi ((E1 /\ E2),X)) | (E1 /\ E2)) . x = (chi ((E1 /\ E2),X)) . x by A2, A3, FUNCT_1:47;
A6: x in E1 /\ E2 by A2, A4, XBOOLE_0:def 4;
then A7: x in E1 by XBOOLE_0:def 4;
((chi (E1,X)) | (E1 /\ E2)) . x = (chi (E1,X)) . x by A4, FUNCT_1:47
.= 1 by A7, FUNCT_3:def 3 ;
hence ((chi (E1,X)) | (E1 /\ E2)) . x = ((chi ((E1 /\ E2),X)) | (E1 /\ E2)) . x by A6, A5, FUNCT_3:def 3; :: thesis: verum
end;
then A8: (chi (E1,X)) | (E1 /\ E2) = (chi ((E1 /\ E2),X)) | (E1 /\ E2) by A2, A3, PARTFUN1:5;
assume M . (E1 /\ E2) < +infty ; :: thesis: Integral (M,((chi (E1,X)) | E2)) = M . (E1 /\ E2)
then A9: Integral (M,((chi (E1,X)) | (E1 /\ E2))) = M . (E1 /\ E2) by A8, Th24;
A10: XX = dom (chi (E1,X)) by FUNCT_3:def 3;
then A11: E2 \ E1 = dom ((chi (E1,X)) | (E2 \ E1)) by RELAT_1:62;
then E2 \ E1 = (dom (chi (E1,X))) /\ (E2 \ E1) by RELAT_1:61;
then A12: (chi (E1,X)) | (E2 \ E1) is E2 \ E1 -measurable by MESFUNC2:29, MESFUNC5:42;
now :: thesis: for x being object st x in dom (chi (E1,X)) holds
0. <= (chi (E1,X)) . x
let x be object ; :: thesis: ( x in dom (chi (E1,X)) implies 0. <= (chi (E1,X)) . x )
assume x in dom (chi (E1,X)) ; :: thesis: 0. <= (chi (E1,X)) . x
then A13: (chi (E1,X)) . x in rng (chi (E1,X)) by FUNCT_1:3;
rng (chi (E1,X)) c= {0,1} by FUNCT_3:39;
hence 0. <= (chi (E1,X)) . x by A13; :: thesis: verum
end;
then A14: chi (E1,X) is nonnegative by SUPINF_2:52;
now :: thesis: for x being Element of X st x in dom ((chi (E1,X)) | (E2 \ E1)) holds
0 = ((chi (E1,X)) | (E2 \ E1)) . x
let x be Element of X; :: thesis: ( x in dom ((chi (E1,X)) | (E2 \ E1)) implies 0 = ((chi (E1,X)) | (E2 \ E1)) . x )
assume A15: x in dom ((chi (E1,X)) | (E2 \ E1)) ; :: thesis: 0 = ((chi (E1,X)) | (E2 \ E1)) . x
E2 \ E1 c= X \ E1 by XBOOLE_1:33;
then (chi (E1,X)) . x = 0 by A11, A15, FUNCT_3:37;
hence 0 = ((chi (E1,X)) | (E2 \ E1)) . x by A15, FUNCT_1:47; :: thesis: verum
end;
then integral+ (M,((chi (E1,X)) | (E2 \ E1))) = 0 by A11, A12, MESFUNC5:87;
then A16: Integral (M,((chi (E1,X)) | (E2 \ E1))) = 0. by A14, A11, A12, MESFUNC5:15, MESFUNC5:88;
chi (E1,X) is XX -measurable by MESFUNC2:29;
then Integral (M,((chi (E1,X)) | E2)) = (Integral (M,((chi (E1,X)) | (E1 /\ E2)))) + (Integral (M,((chi (E1,X)) | (E2 \ E1)))) by A10, A14, A1, MESFUNC5:91, XBOOLE_1:89;
hence Integral (M,((chi (E1,X)) | E2)) = M . (E1 /\ E2) by A9, A16, XXREAL_3:4; :: thesis: verum