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 f being empty PartFunc of [:X1,X2:],ExtREAL
for A being Element of sigma (measurable_rectangles (S1,S2)) holds
( ( M1 is sigma_finite implies Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) ) & ( M2 is sigma_finite implies Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f))) ) )
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 f being empty PartFunc of [:X1,X2:],ExtREAL
for A being Element of sigma (measurable_rectangles (S1,S2)) holds
( ( M1 is sigma_finite implies Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) ) & ( M2 is sigma_finite implies Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f))) ) )
let S2 be SigmaField of X2; :: thesis: for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for f being empty PartFunc of [:X1,X2:],ExtREAL
for A being Element of sigma (measurable_rectangles (S1,S2)) holds
( ( M1 is sigma_finite implies Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) ) & ( M2 is sigma_finite implies Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f))) ) )
let M1 be sigma_Measure of S1; :: thesis: for M2 being sigma_Measure of S2
for f being empty PartFunc of [:X1,X2:],ExtREAL
for A being Element of sigma (measurable_rectangles (S1,S2)) holds
( ( M1 is sigma_finite implies Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) ) & ( M2 is sigma_finite implies Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f))) ) )
let M2 be sigma_Measure of S2; :: thesis: for f being empty PartFunc of [:X1,X2:],ExtREAL
for A being Element of sigma (measurable_rectangles (S1,S2)) holds
( ( M1 is sigma_finite implies Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) ) & ( M2 is sigma_finite implies Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f))) ) )
let f be empty PartFunc of [:X1,X2:],ExtREAL; :: thesis: for A being Element of sigma (measurable_rectangles (S1,S2)) holds
( ( M1 is sigma_finite implies Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) ) & ( M2 is sigma_finite implies Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f))) ) )
let A be Element of sigma (measurable_rectangles (S1,S2)); :: thesis: ( ( M1 is sigma_finite implies Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) ) & ( M2 is sigma_finite implies Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f))) ) )
reconsider EMP = {} 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;
A2: f is_simple_func_in sigma (measurable_rectangles (S1,S2)) by Th19;
A3: f is EMP -measurable by Th19, MESFUNC2:34;
A5: for x being object st x in dom f holds
0 <= f . x ;
then A6: f is nonnegative by SUPINF_2:52;
A4: dom f = EMP ;
then integral' ((Prod_Measure (M1,M2)),f) = 0 by MESFUNC5:def 14;
then A7: Integral ((Prod_Measure (M1,M2)),f) = 0 by A2, A6, MESFUNC5:89;
A8: ( dom (Integral1 (M1,f)) = XX2 & dom (Integral2 (M2,f)) = XX1 ) by FUNCT_2:def 1;
A10: ( Integral1 (M1,f) is nonnegative & Integral2 (M2,f) is nonnegative ) by A3, A4, A6, Th66;

hereby :: thesis: ( M2 is sigma_finite implies Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f))) )

assume M1 is sigma_finite ; :: thesis: Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f)))
then A9: Integral1 (M1,f) is XX2 -measurable by A3, A5, Th59, SUPINF_2:52;
for y being Element of X2 st y in dom (Integral1 (M1,f)) holds
(Integral1 (M1,f)) . y = 0

proof

let y be Element of X2; :: thesis: ( y in dom (Integral1 (M1,f)) implies (Integral1 (M1,f)) . y = 0 )
assume y in dom (Integral1 (M1,f)) ; :: thesis: (Integral1 (M1,f)) . y = 0
A11: ( ProjPMap2 (f,y) is_simple_func_in S1 & ProjPMap2 (f,y) is nonnegative ) by A6, A2, Th31, Th32;
dom f = {} [:X1,X2:] ;
then dom (ProjPMap2 (f,y)) = Y-section (({} [:X1,X2:]),y) by Def4
.= {} by MEASUR11:24 ;
then integral' (M1,(ProjPMap2 (f,y))) = 0 by MESFUNC5:def 14;
then Integral (M1,(ProjPMap2 (f,y))) = 0 by A11, MESFUNC5:89;
hence (Integral1 (M1,f)) . y = 0 by Def7; :: thesis: verum

end;

then integral+ (M2,(Integral1 (M1,f))) = 0 by A8, A9, MESFUNC5:87;
hence Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) by A7, A8, A9, A10, MESFUNC5:88; :: thesis: verum

end;

assume M2 is sigma_finite ; :: thesis: Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f)))
then B9: Integral2 (M2,f) is XX1 -measurable by A3, A5, Th60, SUPINF_2:52;
for x being Element of X1 st x in dom (Integral2 (M2,f)) holds
(Integral2 (M2,f)) . x = 0

proof

let x be Element of X1; :: thesis: ( x in dom (Integral2 (M2,f)) implies (Integral2 (M2,f)) . x = 0 )
assume x in dom (Integral2 (M2,f)) ; :: thesis: (Integral2 (M2,f)) . x = 0
B11: ( ProjPMap1 (f,x) is_simple_func_in S2 & ProjPMap1 (f,x) is nonnegative ) by A6, A2, Th31, Th32;
dom f = {} [:X1,X2:] ;
then dom (ProjPMap1 (f,x)) = X-section (({} [:X1,X2:]),x) by Def3
.= {} by MEASUR11:24 ;
then integral' (M2,(ProjPMap1 (f,x))) = 0 by MESFUNC5:def 14;
then Integral (M2,(ProjPMap1 (f,x))) = 0 by B11, MESFUNC5:89;
hence (Integral2 (M2,f)) . x = 0 by Def8; :: thesis: verum

end;

then integral+ (M1,(Integral2 (M2,f))) = 0 by A8, B9, MESFUNC5:87;
hence Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f))) by A7, A8, B9, A10, MESFUNC5:88; :: thesis: verum