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:21;
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:90
.= 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: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 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:70;
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:70
.= 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:34;
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:91;
then E2 \ E1 = (dom (chi E1,X)) /\ (E2 \ E1) by RELAT_1:90;
then A12: (chi E1,X) | (E2 \ E1) is_measurable_on E2 \ E1 by MESFUNC2:32, MESFUNC5:48;

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 A13: (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 A13; :: thesis: verum

end;

then A14: chi E1,X is nonnegative by SUPINF_2:71;

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 A11, 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 A11, A12, MESFUNC5:93;
then A16: Integral M,((chi E1,X) | (E2 \ E1)) = 0. by A14, A11, A12, MESFUNC5:21, MESFUNC5:94;
chi E1,X is_measurable_on XX by MESFUNC2:32;
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:97, XBOOLE_1:89;
hence Integral M,((chi E1,X) | E2) = M . (E1 /\ E2) by A9, A16, XXREAL_3:4; :: thesis: verum