let X1, X2 be non empty set ; for S1 being SigmaField of X1
for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for E being Element of sigma (measurable_rectangles (S1,S2))
for er being ExtReal holds
( Integral1 (M1,((chi (er,E,[:X1,X2:])) | E)) = Integral1 (M1,(chi (er,E,[:X1,X2:]))) & Integral2 (M2,((chi (er,E,[:X1,X2:])) | E)) = Integral2 (M2,(chi (er,E,[:X1,X2:]))) )
let S1 be SigmaField of X1; for S2 being SigmaField of X2
for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for E being Element of sigma (measurable_rectangles (S1,S2))
for er being ExtReal holds
( Integral1 (M1,((chi (er,E,[:X1,X2:])) | E)) = Integral1 (M1,(chi (er,E,[:X1,X2:]))) & Integral2 (M2,((chi (er,E,[:X1,X2:])) | E)) = Integral2 (M2,(chi (er,E,[:X1,X2:]))) )
let S2 be SigmaField of X2; for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for E being Element of sigma (measurable_rectangles (S1,S2))
for er being ExtReal holds
( Integral1 (M1,((chi (er,E,[:X1,X2:])) | E)) = Integral1 (M1,(chi (er,E,[:X1,X2:]))) & Integral2 (M2,((chi (er,E,[:X1,X2:])) | E)) = Integral2 (M2,(chi (er,E,[:X1,X2:]))) )
let M1 be sigma_Measure of S1; for M2 being sigma_Measure of S2
for E being Element of sigma (measurable_rectangles (S1,S2))
for er being ExtReal holds
( Integral1 (M1,((chi (er,E,[:X1,X2:])) | E)) = Integral1 (M1,(chi (er,E,[:X1,X2:]))) & Integral2 (M2,((chi (er,E,[:X1,X2:])) | E)) = Integral2 (M2,(chi (er,E,[:X1,X2:]))) )
let M2 be sigma_Measure of S2; for E being Element of sigma (measurable_rectangles (S1,S2))
for er being ExtReal holds
( Integral1 (M1,((chi (er,E,[:X1,X2:])) | E)) = Integral1 (M1,(chi (er,E,[:X1,X2:]))) & Integral2 (M2,((chi (er,E,[:X1,X2:])) | E)) = Integral2 (M2,(chi (er,E,[:X1,X2:]))) )
let E be Element of sigma (measurable_rectangles (S1,S2)); for er being ExtReal holds
( Integral1 (M1,((chi (er,E,[:X1,X2:])) | E)) = Integral1 (M1,(chi (er,E,[:X1,X2:]))) & Integral2 (M2,((chi (er,E,[:X1,X2:])) | E)) = Integral2 (M2,(chi (er,E,[:X1,X2:]))) )
let er be ExtReal; ( Integral1 (M1,((chi (er,E,[:X1,X2:])) | E)) = Integral1 (M1,(chi (er,E,[:X1,X2:]))) & Integral2 (M2,((chi (er,E,[:X1,X2:])) | E)) = Integral2 (M2,(chi (er,E,[:X1,X2:]))) )
reconsider XX12 = [:X1,X2:] as Element of sigma (measurable_rectangles (S1,S2)) by MEASURE1:7;
reconsider C = (chi (E,[:X1,X2:])) | E as PartFunc of [:X1,X2:],ExtREAL ;
per cases
( er in REAL or er = +infty or er = -infty )
by XXREAL_0:14;
suppose
er in REAL
;
( Integral1 (M1,((chi (er,E,[:X1,X2:])) | E)) = Integral1 (M1,(chi (er,E,[:X1,X2:]))) & Integral2 (M2,((chi (er,E,[:X1,X2:])) | E)) = Integral2 (M2,(chi (er,E,[:X1,X2:]))) )then reconsider r =
er as
Real ;
A1:
chi (
r,
E,
[:X1,X2:])
= r (#) (chi (E,[:X1,X2:]))
by Th1;
A2:
chi (
E,
[:X1,X2:]) is
XX12 -measurable
by MESFUNC2:29;
A3:
dom (chi (E,[:X1,X2:])) = XX12
by FUNCT_2:def 1;
A4:
dom ((chi (E,[:X1,X2:])) | E) =
(dom (chi (E,[:X1,X2:]))) /\ E
by RELAT_1:61
.=
[:X1,X2:] /\ E
by FUNCT_2:def 1
.=
E
by XBOOLE_1:28
;
A5:
(chi (E,[:X1,X2:])) | E is
nonnegative
by MESFUNC5:15;
E = (dom (chi (E,[:X1,X2:]))) /\ E
by A3, XBOOLE_1:28;
then A6:
(chi (E,[:X1,X2:])) | E is
E -measurable
by MESFUNC2:29, MESFUNC5:42;
Integral1 (
M1,
((chi (r,E,[:X1,X2:])) | E)) =
Integral1 (
M1,
(r (#) C))
by A1, MESFUN11:2
.=
r (#) (Integral1 (M1,C))
by A4, A5, A6, Th78
.=
r (#) (Integral1 (M1,(chi (E,[:X1,X2:]))))
by Th79
.=
Integral1 (
M1,
(r (#) (chi (E,[:X1,X2:]))))
by A2, A3, Th78
;
hence
Integral1 (
M1,
((chi (er,E,[:X1,X2:])) | E))
= Integral1 (
M1,
(chi (er,E,[:X1,X2:])))
by Th1;
Integral2 (M2,((chi (er,E,[:X1,X2:])) | E)) = Integral2 (M2,(chi (er,E,[:X1,X2:]))) Integral2 (
M2,
((chi (r,E,[:X1,X2:])) | E)) =
Integral2 (
M2,
(r (#) C))
by A1, MESFUN11:2
.=
r (#) (Integral2 (M2,C))
by A4, A5, A6, Th78
.=
r (#) (Integral2 (M2,(chi (E,[:X1,X2:]))))
by Th79
.=
Integral2 (
M2,
(r (#) (chi (E,[:X1,X2:]))))
by A2, A3, Th78
;
hence
Integral2 (
M2,
((chi (er,E,[:X1,X2:])) | E))
= Integral2 (
M2,
(chi (er,E,[:X1,X2:])))
by Th1;
verum end; suppose
er = +infty
;
( Integral1 (M1,((chi (er,E,[:X1,X2:])) | E)) = Integral1 (M1,(chi (er,E,[:X1,X2:]))) & Integral2 (M2,((chi (er,E,[:X1,X2:])) | E)) = Integral2 (M2,(chi (er,E,[:X1,X2:]))) )then
chi (
er,
E,
[:X1,X2:])
= Xchi (
E,
[:X1,X2:])
by Th2;
hence
(
Integral1 (
M1,
((chi (er,E,[:X1,X2:])) | E))
= Integral1 (
M1,
(chi (er,E,[:X1,X2:]))) &
Integral2 (
M2,
((chi (er,E,[:X1,X2:])) | E))
= Integral2 (
M2,
(chi (er,E,[:X1,X2:]))) )
by Th80;
verum end; suppose d0:
er = -infty
;
( Integral1 (M1,((chi (er,E,[:X1,X2:])) | E)) = Integral1 (M1,(chi (er,E,[:X1,X2:]))) & Integral2 (M2,((chi (er,E,[:X1,X2:])) | E)) = Integral2 (M2,(chi (er,E,[:X1,X2:]))) )reconsider XX12 =
[:X1,X2:] as
Element of
sigma (measurable_rectangles (S1,S2)) by MEASURE1:7;
reconsider XE =
(Xchi (E,[:X1,X2:])) | E as
PartFunc of
[:X1,X2:],
ExtREAL ;
d3:
Xchi (
E,
[:X1,X2:]) is
XX12 -measurable
by MEASUR10:32;
e2:
XE is
nonnegative
by MESFUNC5:15;
d4:
dom (Xchi (E,[:X1,X2:])) = XX12
by FUNCT_2:def 1;
then e1:
dom XE = E
by RELAT_1:62;
then
E = (dom (Xchi (E,[:X1,X2:]))) /\ E
by RELAT_1:61;
then e3:
XE is
E -measurable
by MESFUNC5:42;
d1:
chi (
er,
E,
[:X1,X2:]) =
- (Xchi (E,[:X1,X2:]))
by d0, Th2
.=
(- 1) (#) (Xchi (E,[:X1,X2:]))
by MESFUNC2:9
;
Integral1 (
M1,
(chi (er,E,[:X1,X2:]))) =
(- 1) (#) (Integral1 (M1,(Xchi (E,[:X1,X2:]))))
by d1, d3, d4, Th78
.=
(- 1) (#) (Integral1 (M1,((Xchi (E,[:X1,X2:])) | E)))
by Th80
.=
Integral1 (
M1,
((- 1) (#) XE))
by e1, e2, e3, Th78
.=
Integral1 (
M1,
((chi (er,E,[:X1,X2:])) | E))
by d1, MESFUN11:2
;
hence
Integral1 (
M1,
((chi (er,E,[:X1,X2:])) | E))
= Integral1 (
M1,
(chi (er,E,[:X1,X2:])))
;
Integral2 (M2,((chi (er,E,[:X1,X2:])) | E)) = Integral2 (M2,(chi (er,E,[:X1,X2:]))) Integral2 (
M2,
(chi (er,E,[:X1,X2:]))) =
(- 1) (#) (Integral2 (M2,(Xchi (E,[:X1,X2:]))))
by d1, d3, d4, Th78
.=
(- 1) (#) (Integral2 (M2,((Xchi (E,[:X1,X2:])) | E)))
by Th80
.=
Integral2 (
M2,
((- 1) (#) XE))
by e1, e2, e3, Th78
.=
Integral2 (
M2,
((chi (er,E,[:X1,X2:])) | E))
by d1, MESFUN11:2
;
hence
Integral2 (
M2,
((chi (er,E,[:X1,X2:])) | E))
= Integral2 (
M2,
(chi (er,E,[:X1,X2:])))
;
verum end;