let X1, X2 be non empty set ; :: thesis: 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,((Xchi (E,[:X1,X2:])) | E)) = Integral1 (M1,(Xchi (E,[:X1,X2:]))) & Integral2 (M2,((Xchi (E,[:X1,X2:])) | E)) = Integral2 (M2,(Xchi (E,[:X1,X2:]))) )
let S1 be SigmaField of X1; :: thesis: 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,((Xchi (E,[:X1,X2:])) | E)) = Integral1 (M1,(Xchi (E,[:X1,X2:]))) & Integral2 (M2,((Xchi (E,[:X1,X2:])) | E)) = Integral2 (M2,(Xchi (E,[:X1,X2:]))) )
let S2 be SigmaField of X2; :: thesis: 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,((Xchi (E,[:X1,X2:])) | E)) = Integral1 (M1,(Xchi (E,[:X1,X2:]))) & Integral2 (M2,((Xchi (E,[:X1,X2:])) | E)) = Integral2 (M2,(Xchi (E,[:X1,X2:]))) )
let M1 be sigma_Measure of S1; :: thesis: for M2 being sigma_Measure of S2
for E being Element of sigma (measurable_rectangles (S1,S2)) holds
( Integral1 (M1,((Xchi (E,[:X1,X2:])) | E)) = Integral1 (M1,(Xchi (E,[:X1,X2:]))) & Integral2 (M2,((Xchi (E,[:X1,X2:])) | E)) = Integral2 (M2,(Xchi (E,[:X1,X2:]))) )
let M2 be sigma_Measure of S2; :: thesis: for E being Element of sigma (measurable_rectangles (S1,S2)) holds
( Integral1 (M1,((Xchi (E,[:X1,X2:])) | E)) = Integral1 (M1,(Xchi (E,[:X1,X2:]))) & Integral2 (M2,((Xchi (E,[:X1,X2:])) | E)) = Integral2 (M2,(Xchi (E,[:X1,X2:]))) )
let E be Element of sigma (measurable_rectangles (S1,S2)); :: thesis: ( Integral1 (M1,((Xchi (E,[:X1,X2:])) | E)) = Integral1 (M1,(Xchi (E,[:X1,X2:]))) & Integral2 (M2,((Xchi (E,[:X1,X2:])) | E)) = Integral2 (M2,(Xchi (E,[:X1,X2:]))) )
now :: thesis: for y being Element of X2 holds (Integral1 (M1,((Xchi (E,[:X1,X2:])) | E))) . y = (Integral1 (M1,(Xchi (E,[:X1,X2:])))) . y
let y be Element of X2; :: thesis: (Integral1 (M1,((Xchi (E,[:X1,X2:])) | E))) . y = (Integral1 (M1,(Xchi (E,[:X1,X2:])))) . y
set XC1 = Xchi ((Measurable-Y-section (E,y)),X1);
A1: ProjPMap2 (((Xchi (E,[:X1,X2:])) | E),y) = (ProjPMap2 ((Xchi (E,[:X1,X2:])),y)) | (Y-section (E,y)) by Th34
.= (Xchi ((Y-section (E,y)),X1)) | (Y-section (E,y)) by Th35
.= (Xchi ((Measurable-Y-section (E,y)),X1)) | (Y-section (E,y)) by MEASUR11:def 7
.= (Xchi ((Measurable-Y-section (E,y)),X1)) | (Measurable-Y-section (E,y)) by MEASUR11:def 7
.= (chi (+infty,(Measurable-Y-section (E,y)),X1)) | (Measurable-Y-section (E,y)) by Th2 ;
(Integral1 (M1,((Xchi (E,[:X1,X2:])) | E))) . y = Integral (M1,(ProjPMap2 (((Xchi (E,[:X1,X2:])) | E),y))) by Def7
.= +infty * (M1 . (Measurable-Y-section (E,y))) by A1, Th50
.= Integral (M1,(chi (+infty,(Measurable-Y-section (E,y)),X1))) by Th49
.= Integral (M1,(Xchi ((Measurable-Y-section (E,y)),X1))) by Th2
.= Integral (M1,(Xchi ((Y-section (E,y)),X1))) by MEASUR11:def 7
.= Integral (M1,(ProjPMap2 ((Xchi (E,[:X1,X2:])),y))) by Th35 ;
hence (Integral1 (M1,((Xchi (E,[:X1,X2:])) | E))) . y = (Integral1 (M1,(Xchi (E,[:X1,X2:])))) . y by Def7; :: thesis: verum
end;
hence Integral1 (M1,((Xchi (E,[:X1,X2:])) | E)) = Integral1 (M1,(Xchi (E,[:X1,X2:]))) by FUNCT_2:def 8; :: thesis: Integral2 (M2,((Xchi (E,[:X1,X2:])) | E)) = Integral2 (M2,(Xchi (E,[:X1,X2:])))
now :: thesis: for x being Element of X1 holds (Integral2 (M2,((Xchi (E,[:X1,X2:])) | E))) . x = (Integral2 (M2,(Xchi (E,[:X1,X2:])))) . x
let x be Element of X1; :: thesis: (Integral2 (M2,((Xchi (E,[:X1,X2:])) | E))) . x = (Integral2 (M2,(Xchi (E,[:X1,X2:])))) . x
set XC2 = Xchi ((Measurable-X-section (E,x)),X2);
A1: ProjPMap1 (((Xchi (E,[:X1,X2:])) | E),x) = (ProjPMap1 ((Xchi (E,[:X1,X2:])),x)) | (X-section (E,x)) by Th34
.= (Xchi ((X-section (E,x)),X2)) | (X-section (E,x)) by Th35
.= (Xchi ((Measurable-X-section (E,x)),X2)) | (X-section (E,x)) by MEASUR11:def 6
.= (Xchi ((Measurable-X-section (E,x)),X2)) | (Measurable-X-section (E,x)) by MEASUR11:def 6
.= (chi (+infty,(Measurable-X-section (E,x)),X2)) | (Measurable-X-section (E,x)) by Th2 ;
(Integral2 (M2,((Xchi (E,[:X1,X2:])) | E))) . x = Integral (M2,(ProjPMap1 (((Xchi (E,[:X1,X2:])) | E),x))) by Def8
.= +infty * (M2 . (Measurable-X-section (E,x))) by A1, Th50
.= Integral (M2,(chi (+infty,(Measurable-X-section (E,x)),X2))) by Th49
.= Integral (M2,(Xchi ((Measurable-X-section (E,x)),X2))) by Th2
.= Integral (M2,(Xchi ((X-section (E,x)),X2))) by MEASUR11:def 6
.= Integral (M2,(ProjPMap1 ((Xchi (E,[:X1,X2:])),x))) by Th35 ;
hence (Integral2 (M2,((Xchi (E,[:X1,X2:])) | E))) . x = (Integral2 (M2,(Xchi (E,[:X1,X2:])))) . x by Def8; :: thesis: verum
end;
hence Integral2 (M2,((Xchi (E,[:X1,X2:])) | E)) = Integral2 (M2,(Xchi (E,[:X1,X2:]))) by FUNCT_2:def 8; :: thesis: verum