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 st M . (E1 /\ E2) < +infty holds
Integral (M,((chi (E1,X)) | E2)) = M . (E1 /\ E2)
let S be 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 M be 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 E1, E2 be Element of S; ( 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 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)) . xlet x be
Element of
X;
( 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))
;
((chi (E1,X)) | (E1 /\ E2)) . x = ((chi ((E1 /\ E2),X)) | (E1 /\ E2)) . xthen 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;
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
; 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;
then A14:
chi (E1,X) is nonnegative
by SUPINF_2:52;
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; verum