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) )
assume A1: M . (E1 /\ E2) < +infty ; :: thesis: Integral M,((chi E1,X) | E2) = M . (E1 /\ E2)
reconsider XX = X as Element of S by MEASURE1:21;
A2: ( XX = dom (chi E1,X) & chi E1,X is_measurable_on XX ) by FUNCT_3:def 3, MESFUNC2:32;

now

let x be set ; :: 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 A3: (chi E1,X) . x in rng (chi E1,X) by FUNCT_1:12;
rng (chi E1,X) c= {0 ,1} by FUNCT_3:48;
hence 0. <= (chi E1,X) . x by A3; :: thesis: verum

end;

then A4: chi E1,X is nonnegative by SUPINF_2:71;
( E1 /\ E2 misses E2 \ E1 & E2 = (E1 /\ E2) \/ (E2 \ E1) ) by XBOOLE_1:51, XBOOLE_1:89;
then A5: Integral M,((chi E1,X) | E2) = (Integral M,((chi E1,X) | (E1 /\ E2))) + (Integral M,((chi E1,X) | (E2 \ E1))) by A2, A4, MESFUNC5:97;
A6: dom ((chi E1,X) | (E1 /\ E2)) = (dom (chi E1,X)) /\ (E1 /\ E2) by RELAT_1:90
.= X /\ (E1 /\ E2) by FUNCT_3:def 3 ;
A7: dom ((chi (E1 /\ E2),X) | (E1 /\ E2)) = (dom (chi (E1 /\ E2),X)) /\ (E1 /\ E2) by RELAT_1:90
.= X /\ (E1 /\ E2) by FUNCT_3:def 3 ;

now

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 A8: x in dom ((chi E1,X) | (E1 /\ E2)) ; :: thesis: ((chi E1,X) | (E1 /\ E2)) . x = ((chi (E1 /\ E2),X) | (E1 /\ E2)) . x
then A9: ( x in X & x in E1 /\ E2 ) by A6, XBOOLE_0:def 4;
then A10: x in E1 by XBOOLE_0:def 4;
A11: ((chi E1,X) | (E1 /\ E2)) . x = (chi E1,X) . x by A8, FUNCT_1:70
.= 1 by A10, FUNCT_3:def 3 ;
((chi (E1 /\ E2),X) | (E1 /\ E2)) . x = (chi (E1 /\ E2),X) . x by A6, A7, A8, FUNCT_1:70;
hence ((chi E1,X) | (E1 /\ E2)) . x = ((chi (E1 /\ E2),X) | (E1 /\ E2)) . x by A9, A11, FUNCT_3:def 3; :: thesis: verum

end;

then (chi E1,X) | (E1 /\ E2) = (chi (E1 /\ E2),X) | (E1 /\ E2) by A6, A7, PARTFUN1:34;
then A12: Integral M,((chi E1,X) | (E1 /\ E2)) = M . (E1 /\ E2) by A1, Th24;
set F = E2 \ E1;
A13: E2 \ E1 = dom ((chi E1,X) | (E2 \ E1)) by A2, RELAT_1:91;
then E2 \ E1 = (dom (chi E1,X)) /\ (E2 \ E1) by RELAT_1:90;
then A14: (chi E1,X) | (E2 \ E1) is_measurable_on E2 \ E1 by MESFUNC2:32, MESFUNC5:48;

now

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 A13, A15, FUNCT_3:43;
hence 0 = ((chi E1,X) | (E2 \ E1)) . x by A15, FUNCT_1:70; :: thesis: verum

end;

then integral+ M,((chi E1,X) | (E2 \ E1)) = 0 by A13, A14, MESFUNC5:93;
then Integral M,((chi E1,X) | (E2 \ E1)) = 0. by A4, A13, A14, MESFUNC5:21, MESFUNC5:94;
hence Integral M,((chi E1,X) | E2) = M . (E1 /\ E2) by A5, A12, XXREAL_3:4; :: thesis: verum