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)) holds
( Integral1 (M1,((chi (E,[:X1,X2:])) | E)) = Integral1 (M1,(chi (E,[:X1,X2:]))) & Integral2 (M2,((chi (E,[:X1,X2:])) | E)) = Integral2 (M2,(chi (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)) holds
( Integral1 (M1,((chi (E,[:X1,X2:])) | E)) = Integral1 (M1,(chi (E,[:X1,X2:]))) & Integral2 (M2,((chi (E,[:X1,X2:])) | E)) = Integral2 (M2,(chi (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)) holds
( Integral1 (M1,((chi (E,[:X1,X2:])) | E)) = Integral1 (M1,(chi (E,[:X1,X2:]))) & Integral2 (M2,((chi (E,[:X1,X2:])) | E)) = Integral2 (M2,(chi (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)) holds
( Integral1 (M1,((chi (E,[:X1,X2:])) | E)) = Integral1 (M1,(chi (E,[:X1,X2:]))) & Integral2 (M2,((chi (E,[:X1,X2:])) | E)) = Integral2 (M2,(chi (E,[:X1,X2:]))) )
let M2 be sigma_Measure of S2; for E being Element of sigma (measurable_rectangles (S1,S2)) holds
( Integral1 (M1,((chi (E,[:X1,X2:])) | E)) = Integral1 (M1,(chi (E,[:X1,X2:]))) & Integral2 (M2,((chi (E,[:X1,X2:])) | E)) = Integral2 (M2,(chi (E,[:X1,X2:]))) )
let E be Element of sigma (measurable_rectangles (S1,S2)); ( Integral1 (M1,((chi (E,[:X1,X2:])) | E)) = Integral1 (M1,(chi (E,[:X1,X2:]))) & Integral2 (M2,((chi (E,[:X1,X2:])) | E)) = Integral2 (M2,(chi (E,[:X1,X2:]))) )
now for y being Element of X2 holds (Integral1 (M1,((chi (E,[:X1,X2:])) | E))) . y = (Integral1 (M1,(chi (E,[:X1,X2:])))) . ylet y be
Element of
X2;
(Integral1 (M1,((chi (E,[:X1,X2:])) | E))) . y = (Integral1 (M1,(chi (E,[:X1,X2:])))) . yA1:
ProjPMap2 (
((chi (E,[:X1,X2:])) | E),
y) =
(ProjPMap2 ((chi (E,[:X1,X2:])),y)) | (Y-section (E,y))
by Th34
.=
(chi ((Y-section (E,y)),X1)) | (Y-section (E,y))
by Th48
.=
(chi ((Measurable-Y-section (E,y)),X1)) | (Y-section (E,y))
by MEASUR11:def 7
.=
(chi ((Measurable-Y-section (E,y)),X1)) | (Measurable-Y-section (E,y))
by MEASUR11:def 7
;
(Integral1 (M1,((chi (E,[:X1,X2:])) | E))) . y =
Integral (
M1,
(ProjPMap2 (((chi (E,[:X1,X2:])) | E),y)))
by Def7
.=
M1 . (Measurable-Y-section (E,y))
by A1, MESFUNC9:14
.=
Integral (
M1,
(chi ((Measurable-Y-section (E,y)),X1)))
by MESFUNC9:14
.=
Integral (
M1,
(chi ((Y-section (E,y)),X1)))
by MEASUR11:def 7
.=
Integral (
M1,
(ProjPMap2 ((chi (E,[:X1,X2:])),y)))
by Th48
;
hence
(Integral1 (M1,((chi (E,[:X1,X2:])) | E))) . y = (Integral1 (M1,(chi (E,[:X1,X2:])))) . y
by Def7;
verum end;
hence
Integral1 (M1,((chi (E,[:X1,X2:])) | E)) = Integral1 (M1,(chi (E,[:X1,X2:])))
by FUNCT_2:def 8; Integral2 (M2,((chi (E,[:X1,X2:])) | E)) = Integral2 (M2,(chi (E,[:X1,X2:])))
now for x being Element of X1 holds (Integral2 (M2,((chi (E,[:X1,X2:])) | E))) . x = (Integral2 (M2,(chi (E,[:X1,X2:])))) . xlet x be
Element of
X1;
(Integral2 (M2,((chi (E,[:X1,X2:])) | E))) . x = (Integral2 (M2,(chi (E,[:X1,X2:])))) . xA2:
ProjPMap1 (
((chi (E,[:X1,X2:])) | E),
x) =
(ProjPMap1 ((chi (E,[:X1,X2:])),x)) | (X-section (E,x))
by Th34
.=
(chi ((X-section (E,x)),X2)) | (X-section (E,x))
by Th48
.=
(chi ((Measurable-X-section (E,x)),X2)) | (X-section (E,x))
by MEASUR11:def 6
.=
(chi ((Measurable-X-section (E,x)),X2)) | (Measurable-X-section (E,x))
by MEASUR11:def 6
;
(Integral2 (M2,((chi (E,[:X1,X2:])) | E))) . x =
Integral (
M2,
(ProjPMap1 (((chi (E,[:X1,X2:])) | E),x)))
by Def8
.=
M2 . (Measurable-X-section (E,x))
by A2, MESFUNC9:14
.=
Integral (
M2,
(chi ((Measurable-X-section (E,x)),X2)))
by MESFUNC9:14
.=
Integral (
M2,
(chi ((X-section (E,x)),X2)))
by MEASUR11:def 6
.=
Integral (
M2,
(ProjPMap1 ((chi (E,[:X1,X2:])),x)))
by Th48
;
hence
(Integral2 (M2,((chi (E,[:X1,X2:])) | E))) . x = (Integral2 (M2,(chi (E,[:X1,X2:])))) . x
by Def8;
verum end;
hence
Integral2 (M2,((chi (E,[:X1,X2:])) | E)) = Integral2 (M2,(chi (E,[:X1,X2:])))
by FUNCT_2:def 8; verum