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))
for r being Real st M1 is sigma_finite & M2 is sigma_finite holds
( Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M2,(Integral1 (M1,(chi (r,E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M2,(Integral1 (M1,((chi (r,E,[:X1,X2:])) | E)))) & Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M1,(Integral2 (M2,(chi (r,E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M1,(Integral2 (M2,((chi (r,E,[:X1,X2:])) | E)))) )
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))
for r being Real st M1 is sigma_finite & M2 is sigma_finite holds
( Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M2,(Integral1 (M1,(chi (r,E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M2,(Integral1 (M1,((chi (r,E,[:X1,X2:])) | E)))) & Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M1,(Integral2 (M2,(chi (r,E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M1,(Integral2 (M2,((chi (r,E,[:X1,X2:])) | E)))) )
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))
for r being Real st M1 is sigma_finite & M2 is sigma_finite holds
( Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M2,(Integral1 (M1,(chi (r,E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M2,(Integral1 (M1,((chi (r,E,[:X1,X2:])) | E)))) & Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M1,(Integral2 (M2,(chi (r,E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M1,(Integral2 (M2,((chi (r,E,[:X1,X2:])) | E)))) )
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))
for r being Real st M1 is sigma_finite & M2 is sigma_finite holds
( Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M2,(Integral1 (M1,(chi (r,E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M2,(Integral1 (M1,((chi (r,E,[:X1,X2:])) | E)))) & Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M1,(Integral2 (M2,(chi (r,E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M1,(Integral2 (M2,((chi (r,E,[:X1,X2:])) | E)))) )
let M2 be sigma_Measure of S2; :: thesis: for E being Element of sigma (measurable_rectangles (S1,S2))
for r being Real st M1 is sigma_finite & M2 is sigma_finite holds
( Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M2,(Integral1 (M1,(chi (r,E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M2,(Integral1 (M1,((chi (r,E,[:X1,X2:])) | E)))) & Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M1,(Integral2 (M2,(chi (r,E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M1,(Integral2 (M2,((chi (r,E,[:X1,X2:])) | E)))) )
let E be Element of sigma (measurable_rectangles (S1,S2)); :: thesis: for r being Real st M1 is sigma_finite & M2 is sigma_finite holds
( Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M2,(Integral1 (M1,(chi (r,E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M2,(Integral1 (M1,((chi (r,E,[:X1,X2:])) | E)))) & Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M1,(Integral2 (M2,(chi (r,E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M1,(Integral2 (M2,((chi (r,E,[:X1,X2:])) | E)))) )
let r be Real; :: thesis: ( M1 is sigma_finite & M2 is sigma_finite implies ( Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M2,(Integral1 (M1,(chi (r,E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M2,(Integral1 (M1,((chi (r,E,[:X1,X2:])) | E)))) & Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M1,(Integral2 (M2,(chi (r,E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M1,(Integral2 (M2,((chi (r,E,[:X1,X2:])) | E)))) ) )
assume that
A1: M1 is sigma_finite and
A2: M2 is sigma_finite ; :: thesis: ( Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M2,(Integral1 (M1,(chi (r,E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M2,(Integral1 (M1,((chi (r,E,[:X1,X2:])) | E)))) & Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M1,(Integral2 (M2,(chi (r,E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M1,(Integral2 (M2,((chi (r,E,[:X1,X2:])) | E)))) )
set S = sigma (measurable_rectangles (S1,S2));
set M = Prod_Measure (M1,M2);
reconsider XX12 = [:X1,X2:] as Element of sigma (measurable_rectangles (S1,S2)) by MEASURE1:7;
reconsider XX1 = X1 as Element of S1 by MEASURE1:7;
reconsider XX2 = X2 as Element of S2 by MEASURE1:7;
A3: chi (r,E,[:X1,X2:]) = r (#) (chi (E,[:X1,X2:])) by Th1;
A4: chi (E,[:X1,X2:]) is_simple_func_in sigma (measurable_rectangles (S1,S2)) by Th12;
A5: chi (E,[:X1,X2:]) is XX12 -measurable by Th12, MESFUNC2:34;
A6: dom (chi (E,[:X1,X2:])) = XX12 by FUNCT_2:def 1;
A7: Integral1 (M1,(chi (E,[:X1,X2:]))) = X-vol (E,M1) by A1, Th64;
A8: X-vol (E,M1) is XX2 -measurable by A1, MEASUR11:def 14;
A9: dom (Integral1 (M1,(chi (E,[:X1,X2:])))) = XX2 by FUNCT_2:def 1;
A10: Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral ((Prod_Measure (M1,M2)),(r (#) (chi (E,[:X1,X2:])))) by Th1
.= r * (integral' ((Prod_Measure (M1,M2)),(chi (E,[:X1,X2:])))) by Th12, MESFUN11:59
.= r * (Integral ((Prod_Measure (M1,M2)),(chi (E,[:X1,X2:])))) by A4, MESFUNC5:89 ;
then A14: Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = r * (Integral (M2,(Integral1 (M1,(chi (E,[:X1,X2:])))))) by A1, A2, Th82
.= Integral (M2,(r (#) (X-vol (E,M1)))) by A7, A8, A9, Lm1 ;
hence Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M2,(Integral1 (M1,(chi (r,E,[:X1,X2:]))))) by A3, A5, A6, A7, Th78; :: thesis: ( Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M2,(Integral1 (M1,((chi (r,E,[:X1,X2:])) | E)))) & Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M1,(Integral2 (M2,(chi (r,E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M1,(Integral2 (M2,((chi (r,E,[:X1,X2:])) | E)))) )
reconsider C = (chi (E,[:X1,X2:])) | E as PartFunc of [:X1,X2:],ExtREAL ;
A11: dom C = E by A6, RELAT_1:62;
A12: (chi (r,E,[:X1,X2:])) | E = (r (#) (chi (E,[:X1,X2:]))) | E by Th1
.= r (#) C by MESFUN11:2 ;
A13: Integral (M2,(Integral1 (M1,((chi (r,E,[:X1,X2:])) | E)))) = Integral (M2,(Integral1 (M1,(chi (r,E,[:X1,X2:]))))) by Th81
.= Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) by A3, A5, A6, A7, A14, Th78 ;
C is E -measurable by A4, MESFUNC2:34, MESFUNC5:34;
then A15: Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = r * (Integral ((Prod_Measure (M1,M2)),C)) by A11, A12, Lm1, MESFUNC5:15
.= r * ((Prod_Measure (M1,M2)) . E) by MESFUNC9:14
.= r * (Integral ((Prod_Measure (M1,M2)),(chi (E,[:X1,X2:])))) by MESFUNC9:14
.= Integral ((Prod_Measure (M1,M2)),(r (#) (chi (E,[:X1,X2:])))) by A4, A6, Lm1, MESFUNC2:34 ;
hence Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M2,(Integral1 (M1,((chi (r,E,[:X1,X2:])) | E)))) by A13, Th1; :: thesis: ( Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M1,(Integral2 (M2,(chi (r,E,[:X1,X2:]))))) & Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M1,(Integral2 (M2,((chi (r,E,[:X1,X2:])) | E)))) )
B7: Integral2 (M2,(chi (E,[:X1,X2:]))) = Y-vol (E,M2) by A2, Th65;
B8: Y-vol (E,M2) is XX1 -measurable by A2, MEASUR11:def 13;
B9: dom (Integral2 (M2,(chi (E,[:X1,X2:])))) = XX1 by FUNCT_2:def 1;
B14: Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = r * (Integral (M1,(Integral2 (M2,(chi (E,[:X1,X2:])))))) by A1, A2, A10, Th82
.= Integral (M1,(r (#) (Y-vol (E,M2)))) by B7, B8, B9, Lm1 ;
hence Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) = Integral (M1,(Integral2 (M2,(chi (r,E,[:X1,X2:]))))) by A3, A5, A6, B7, Th78; :: thesis: Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M1,(Integral2 (M2,((chi (r,E,[:X1,X2:])) | E))))
Integral (M1,(Integral2 (M2,((chi (r,E,[:X1,X2:])) | E)))) = Integral (M1,(Integral2 (M2,(chi (r,E,[:X1,X2:]))))) by Th81
.= Integral ((Prod_Measure (M1,M2)),(chi (r,E,[:X1,X2:]))) by A3, A5, A6, B7, B14, Th78 ;
hence Integral ((Prod_Measure (M1,M2)),((chi (r,E,[:X1,X2:])) | E)) = Integral (M1,(Integral2 (M2,((chi (r,E,[:X1,X2:])) | E)))) by A15, Th1; :: thesis: verum