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 non empty PartFunc of [:X1,X2:],ExtREAL
for A being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite & M2 is sigma_finite & f is_simple_func_in sigma (measurable_rectangles (S1,S2)) & ( f is nonnegative or f is nonpositive ) & A = dom f holds
( Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) & 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 non empty PartFunc of [:X1,X2:],ExtREAL
for A being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite & M2 is sigma_finite & f is_simple_func_in sigma (measurable_rectangles (S1,S2)) & ( f is nonnegative or f is nonpositive ) & A = dom f holds
( Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) & 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 non empty PartFunc of [:X1,X2:],ExtREAL
for A being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite & M2 is sigma_finite & f is_simple_func_in sigma (measurable_rectangles (S1,S2)) & ( f is nonnegative or f is nonpositive ) & A = dom f holds
( Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) & 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 non empty PartFunc of [:X1,X2:],ExtREAL
for A being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite & M2 is sigma_finite & f is_simple_func_in sigma (measurable_rectangles (S1,S2)) & ( f is nonnegative or f is nonpositive ) & A = dom f holds
( Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) & Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f))) )
let M2 be sigma_Measure of S2; :: thesis: for f being non empty PartFunc of [:X1,X2:],ExtREAL
for A being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite & M2 is sigma_finite & f is_simple_func_in sigma (measurable_rectangles (S1,S2)) & ( f is nonnegative or f is nonpositive ) & A = dom f holds
( Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) & Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f))) )
let f be non empty PartFunc of [:X1,X2:],ExtREAL; :: thesis: for A being Element of sigma (measurable_rectangles (S1,S2)) st M1 is sigma_finite & M2 is sigma_finite & f is_simple_func_in sigma (measurable_rectangles (S1,S2)) & ( f is nonnegative or f is nonpositive ) & A = dom f holds
( Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) & 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 & M2 is sigma_finite & f is_simple_func_in sigma (measurable_rectangles (S1,S2)) & ( f is nonnegative or f is nonpositive ) & A = dom f implies ( Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) & Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f))) ) )
assume that
A1: M1 is sigma_finite and
A2: M2 is sigma_finite and
A3: f is_simple_func_in sigma (measurable_rectangles (S1,S2)) and
A4: ( f is nonnegative or f is nonpositive ) and
A5: A = dom f ; :: thesis: ( Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) & Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f))) )
A6: f is A -measurable by A3, MESFUNC2:34;
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;
consider E being non empty Finite_Sep_Sequence of sigma (measurable_rectangles (S1,S2)), a being FinSequence of ExtREAL , r being FinSequence of REAL such that
A7: ( E,a are_Re-presentation_of f & ( for n being Nat holds
( a . n = r . n & f | (E . n) = (chi ((r . n),(E . n),[:X1,X2:])) | (E . n) & ( E . n = {} implies r . n = 0 ) ) ) ) by A3, Th5;
defpred S1[ Nat] means Integral ((Prod_Measure (M1,M2)),(f | (union (rng (E | $1))))) = Integral (M2,(Integral1 (M1,(f | (union (rng (E | $1)))))));
A8: S1[ 0 ]
proof
reconsider E0 = {} as Element of sigma (measurable_rectangles (S1,S2)) by MEASURE1:7;
reconsider E01 = {} as Element of S1 by MEASURE1:7;
(Prod_Measure (M1,M2)) . E0 = 0 by VALUED_0:def 19;
then A9: Integral ((Prod_Measure (M1,M2)),(f | (union (rng (E | 0))))) = 0 by A3, A5, MESFUNC2:34, ZFMISC_1:2, MESFUNC5:94;
A10: for y being Element of X2 st y in dom (Integral1 (M1,(f | (union (rng (E | 0)))))) holds
(Integral1 (M1,(f | (union (rng (E | 0)))))) . y = 0
proof
let y be Element of X2; :: thesis: ( y in dom (Integral1 (M1,(f | (union (rng (E | 0)))))) implies (Integral1 (M1,(f | (union (rng (E | 0)))))) . y = 0 )
assume y in dom (Integral1 (M1,(f | (union (rng (E | 0)))))) ; :: thesis: (Integral1 (M1,(f | (union (rng (E | 0)))))) . y = 0
(Integral1 (M1,(f | (union (rng (E | 0)))))) . y = Integral (M1,(ProjPMap2 ((f | (union (rng (E | 0)))),y))) by Def7;
then A11: (Integral1 (M1,(f | (union (rng (E | 0)))))) . y = Integral (M1,((ProjPMap2 (f,y)) | (Y-section (E0,y)))) by Th34, ZFMISC_1:2;
A12: M1 . E01 = 0 by VALUED_0:def 19;
dom (ProjPMap2 (f,y)) = Y-section ((dom f),y) by Def4;
then A13: dom (ProjPMap2 (f,y)) = Measurable-Y-section (A,y) by A5, MEASUR11:def 7;
E0 = {} [:X1,X2:] ;
then (Integral1 (M1,(f | (union (rng (E | 0)))))) . y = Integral (M1,((ProjPMap2 (f,y)) | E01)) by A11, MEASUR11:24;
hence (Integral1 (M1,(f | (union (rng (E | 0)))))) . y = 0 by A5, A6, A12, A13, Th47, MESFUNC5:94; :: thesis: verum
end;
dom (Integral1 (M1,(f | (union (rng (E | 0)))))) = XX2 by FUNCT_2:def 1;
hence S1[ 0 ] by A9, A10, Th57; :: thesis: verum
end;
A14: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A15: S1[n] ; :: thesis: S1[n + 1]
per cases ( n >= len E or n < len E ) ;
suppose n >= len E ; :: thesis: S1[n + 1]
then ( E | n = E & E | (n + 1) = E ) by FINSEQ_1:58, NAT_1:12;
hence Integral ((Prod_Measure (M1,M2)),(f | (union (rng (E | (n + 1)))))) = Integral (M2,(Integral1 (M1,(f | (union (rng (E | (n + 1)))))))) by A15; :: thesis: verum
end;
suppose n < len E ; :: thesis: S1[n + 1]
Union (E | n) is Element of sigma (measurable_rectangles (S1,S2)) ;
then reconsider En = union (rng (E | n)) as Element of sigma (measurable_rectangles (S1,S2)) by CARD_3:def 4;
reconsider En1 = E . (n + 1) as Element of sigma (measurable_rectangles (S1,S2)) ;
A16: ( En misses En1 & union (rng (E | (n + 1))) = En \/ En1 ) by NAT_1:16, MEASUR11:1, MEASUR11:3;
set CH = chi ((r . (n + 1)),(E . (n + 1)),[:X1,X2:]);
A17: Integral ((Prod_Measure (M1,M2)),((chi ((r . (n + 1)),(E . (n + 1)),[:X1,X2:])) | (E . (n + 1)))) = Integral (M2,(Integral1 (M1,((chi ((r . (n + 1)),(E . (n + 1)),[:X1,X2:])) | (E . (n + 1)))))) by A1, A2, Th83;
A18: ( dom (Integral1 (M1,(f | En))) = XX2 & dom (Integral1 (M1,(f | En1))) = XX2 ) by FUNCT_2:def 1;
A19: ( Integral1 (M1,(f | En)) is XX2 -measurable & Integral1 (M1,(f | En1)) is XX2 -measurable ) by A1, A4, A5, A6, Th68;
A20: ( (Integral1 (M1,(f | En))) | XX2 = Integral1 (M1,(f | En)) & (Integral1 (M1,(f | En1))) | XX2 = Integral1 (M1,(f | En1)) ) ;
Integral ((Prod_Measure (M1,M2)),(f | En1)) = Integral ((Prod_Measure (M1,M2)),((chi ((r . (n + 1)),(E . (n + 1)),[:X1,X2:])) | (E . (n + 1)))) by A7;
then A21: Integral ((Prod_Measure (M1,M2)),(f | En1)) = Integral (M2,(Integral1 (M1,(f | En1)))) by A7, A17;
per cases ( f is nonnegative or f is nonpositive ) by A4;
suppose A22: f is nonnegative ; :: thesis: S1[n + 1]
then A23: ( Integral1 (M1,(f | En)) is nonnegative & Integral1 (M1,(f | En1)) is nonnegative ) by A5, A6, Th66;
then reconsider I1 = Integral1 (M1,(f | En)), I2 = Integral1 (M1,(f | En1)) as without-infty Function of X2,ExtREAL ;
I1 + I2 = (Integral1 (M1,(f | En))) + (Integral1 (M1,(f | En1))) ;
then A24: dom ((Integral1 (M1,(f | En))) + (Integral1 (M1,(f | En1)))) = XX2 by FUNCT_2:def 1;
Integral ((Prod_Measure (M1,M2)),(f | (union (rng (E | (n + 1)))))) = (Integral ((Prod_Measure (M1,M2)),(f | En))) + (Integral ((Prod_Measure (M1,M2)),(f | En1))) by A3, A5, A22, A16, MESFUNC2:34, MESFUNC5:91;
then Integral ((Prod_Measure (M1,M2)),(f | (union (rng (E | (n + 1)))))) = Integral (M2,((Integral1 (M1,(f | En))) + (Integral1 (M1,(f | En1))))) by A15, A18, A19, A20, A21, A23, A24, Th21;
hence Integral ((Prod_Measure (M1,M2)),(f | (union (rng (E | (n + 1)))))) = Integral (M2,(Integral1 (M1,(f | (union (rng (E | (n + 1)))))))) by A5, A6, A16, A22, Lm11; :: thesis: verum
end;
suppose A25: f is nonpositive ; :: thesis: S1[n + 1]
then A26: ( Integral1 (M1,(f | En)) is nonpositive & Integral1 (M1,(f | En1)) is nonpositive ) by A5, A6, Th67;
then reconsider I1 = Integral1 (M1,(f | En)), I2 = Integral1 (M1,(f | En1)) as without+infty Function of X2,ExtREAL ;
I1 + I2 = (Integral1 (M1,(f | En))) + (Integral1 (M1,(f | En1))) ;
then A27: dom ((Integral1 (M1,(f | En))) + (Integral1 (M1,(f | En1)))) = XX2 by FUNCT_2:def 1;
Integral ((Prod_Measure (M1,M2)),(f | (union (rng (E | (n + 1)))))) = (Integral ((Prod_Measure (M1,M2)),(f | En))) + (Integral ((Prod_Measure (M1,M2)),(f | En1))) by A3, A5, A16, A25, MESFUNC2:34, MESFUN11:62;
then Integral ((Prod_Measure (M1,M2)),(f | (union (rng (E | (n + 1)))))) = Integral (M2,((Integral1 (M1,(f | En))) + (Integral1 (M1,(f | En1))))) by A15, A18, A19, A20, A21, A26, A27, Th22;
hence Integral ((Prod_Measure (M1,M2)),(f | (union (rng (E | (n + 1)))))) = Integral (M2,(Integral1 (M1,(f | (union (rng (E | (n + 1)))))))) by A5, A6, A16, A25, Lm12; :: thesis: verum
end;
end;
end;
end;
end;
A28: union (rng E) = dom f by A7, MESFUNC3:def 1;
for n being Nat holds S1[n] from NAT_1:sch 2(A8, A14);
 then Integral ((Prod_Measure (M1,M2)),(f | (union (rng (E | (len E)))))) = Integral (M2,(Integral1 (M1,(f | (union (rng (E | (len E)))))))) ;
then Integral ((Prod_Measure (M1,M2)),(f | (union (rng E)))) = Integral (M2,(Integral1 (M1,(f | (union (rng (E | (len E)))))))) by FINSEQ_1:58;
hence Integral ((Prod_Measure (M1,M2)),f) = Integral (M2,(Integral1 (M1,f))) by A28, FINSEQ_1:58; :: thesis: Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f)))
defpred S2[ Nat] means Integral ((Prod_Measure (M1,M2)),(f | (union (rng (E | $1))))) = Integral (M1,(Integral2 (M2,(f | (union (rng (E | $1)))))));
A8: S2[ 0 ]
proof
reconsider E0 = {} as Element of sigma (measurable_rectangles (S1,S2)) by MEASURE1:7;
reconsider E01 = {} as Element of S2 by MEASURE1:7;
(Prod_Measure (M1,M2)) . E0 = 0 by VALUED_0:def 19;
then A9: Integral ((Prod_Measure (M1,M2)),(f | (union (rng (E | 0))))) = 0 by A3, A5, MESFUNC2:34, ZFMISC_1:2, MESFUNC5:94;
A10: for x being Element of X1 st x in dom (Integral2 (M2,(f | (union (rng (E | 0)))))) holds
(Integral2 (M2,(f | (union (rng (E | 0)))))) . x = 0
proof
let x be Element of X1; :: thesis: ( x in dom (Integral2 (M2,(f | (union (rng (E | 0)))))) implies (Integral2 (M2,(f | (union (rng (E | 0)))))) . x = 0 )
assume x in dom (Integral2 (M2,(f | (union (rng (E | 0)))))) ; :: thesis: (Integral2 (M2,(f | (union (rng (E | 0)))))) . x = 0
(Integral2 (M2,(f | (union (rng (E | 0)))))) . x = Integral (M2,(ProjPMap1 ((f | (union (rng (E | 0)))),x))) by Def8;
then A11: (Integral2 (M2,(f | (union (rng (E | 0)))))) . x = Integral (M2,((ProjPMap1 (f,x)) | (X-section (E0,x)))) by Th34, ZFMISC_1:2;
A12: M2 . E01 = 0 by VALUED_0:def 19;
dom (ProjPMap1 (f,x)) = X-section ((dom f),x) by Def3;
then A13: dom (ProjPMap1 (f,x)) = Measurable-X-section (A,x) by A5, MEASUR11:def 6;
E0 = {} [:X1,X2:] ;
then (Integral2 (M2,(f | (union (rng (E | 0)))))) . x = Integral (M2,((ProjPMap1 (f,x)) | E01)) by A11, MEASUR11:24;
hence (Integral2 (M2,(f | (union (rng (E | 0)))))) . x = 0 by A5, A6, A12, A13, Th47, MESFUNC5:94; :: thesis: verum
end;
dom (Integral2 (M2,(f | (union (rng (E | 0)))))) = XX1 by FUNCT_2:def 1;
hence S2[ 0 ] by A9, A10, Th57; :: thesis: verum
end;
A14: for n being Nat st S2[n] holds
S2[n + 1]
proof
let n be Nat; :: thesis: ( S2[n] implies S2[n + 1] )
assume A15: S2[n] ; :: thesis: S2[n + 1]
per cases ( n >= len E or n < len E ) ;
suppose n >= len E ; :: thesis: S2[n + 1]
then ( E | n = E & E | (n + 1) = E ) by FINSEQ_1:58, NAT_1:12;
hence Integral ((Prod_Measure (M1,M2)),(f | (union (rng (E | (n + 1)))))) = Integral (M1,(Integral2 (M2,(f | (union (rng (E | (n + 1)))))))) by A15; :: thesis: verum
end;
suppose n < len E ; :: thesis: S2[n + 1]
Union (E | n) is Element of sigma (measurable_rectangles (S1,S2)) ;
then reconsider En = union (rng (E | n)) as Element of sigma (measurable_rectangles (S1,S2)) by CARD_3:def 4;
reconsider En1 = E . (n + 1) as Element of sigma (measurable_rectangles (S1,S2)) ;
A16: ( En misses En1 & union (rng (E | (n + 1))) = En \/ En1 ) by NAT_1:16, MEASUR11:1, MEASUR11:3;
set CH = chi ((r . (n + 1)),(E . (n + 1)),[:X1,X2:]);
A17: Integral ((Prod_Measure (M1,M2)),((chi ((r . (n + 1)),(E . (n + 1)),[:X1,X2:])) | (E . (n + 1)))) = Integral (M1,(Integral2 (M2,((chi ((r . (n + 1)),(E . (n + 1)),[:X1,X2:])) | (E . (n + 1)))))) by A1, A2, Th83;
A18: ( dom (Integral2 (M2,(f | En))) = XX1 & dom (Integral2 (M2,(f | En1))) = XX1 ) by FUNCT_2:def 1;
A19: ( Integral2 (M2,(f | En)) is XX1 -measurable & Integral2 (M2,(f | En1)) is XX1 -measurable ) by A2, A4, A5, A6, Th69;
A20: ( (Integral2 (M2,(f | En))) | XX1 = Integral2 (M2,(f | En)) & (Integral2 (M2,(f | En1))) | XX1 = Integral2 (M2,(f | En1)) ) ;
Integral ((Prod_Measure (M1,M2)),(f | En1)) = Integral ((Prod_Measure (M1,M2)),((chi ((r . (n + 1)),(E . (n + 1)),[:X1,X2:])) | (E . (n + 1)))) by A7;
then A21: Integral ((Prod_Measure (M1,M2)),(f | En1)) = Integral (M1,(Integral2 (M2,(f | En1)))) by A7, A17;
per cases ( f is nonnegative or f is nonpositive ) by A4;
suppose A22: f is nonnegative ; :: thesis: S2[n + 1]
then A23: ( Integral2 (M2,(f | En)) is nonnegative & Integral2 (M2,(f | En1)) is nonnegative ) by A5, A6, Th66;
then reconsider I1 = Integral2 (M2,(f | En)), I2 = Integral2 (M2,(f | En1)) as without-infty Function of X1,ExtREAL ;
I1 + I2 = (Integral2 (M2,(f | En))) + (Integral2 (M2,(f | En1))) ;
then A24: dom ((Integral2 (M2,(f | En))) + (Integral2 (M2,(f | En1)))) = XX1 by FUNCT_2:def 1;
Integral ((Prod_Measure (M1,M2)),(f | (union (rng (E | (n + 1)))))) = (Integral ((Prod_Measure (M1,M2)),(f | En))) + (Integral ((Prod_Measure (M1,M2)),(f | En1))) by A3, A5, A22, A16, MESFUNC2:34, MESFUNC5:91;
then Integral ((Prod_Measure (M1,M2)),(f | (union (rng (E | (n + 1)))))) = Integral (M1,((Integral2 (M2,(f | En))) + (Integral2 (M2,(f | En1))))) by A15, A18, A19, A20, A21, A23, A24, Th21;
hence Integral ((Prod_Measure (M1,M2)),(f | (union (rng (E | (n + 1)))))) = Integral (M1,(Integral2 (M2,(f | (union (rng (E | (n + 1)))))))) by A5, A6, A16, A22, Lm11; :: thesis: verum
end;
suppose A25: f is nonpositive ; :: thesis: S2[n + 1]
then A26: ( Integral2 (M2,(f | En)) is nonpositive & Integral2 (M2,(f | En1)) is nonpositive ) by A5, A6, Th67;
then reconsider I1 = Integral2 (M2,(f | En)), I2 = Integral2 (M2,(f | En1)) as without+infty Function of X1,ExtREAL ;
I1 + I2 = (Integral2 (M2,(f | En))) + (Integral2 (M2,(f | En1))) ;
then A27: dom ((Integral2 (M2,(f | En))) + (Integral2 (M2,(f | En1)))) = XX1 by FUNCT_2:def 1;
Integral ((Prod_Measure (M1,M2)),(f | (union (rng (E | (n + 1)))))) = (Integral ((Prod_Measure (M1,M2)),(f | En))) + (Integral ((Prod_Measure (M1,M2)),(f | En1))) by A3, A5, A16, A25, MESFUNC2:34, MESFUN11:62;
then Integral ((Prod_Measure (M1,M2)),(f | (union (rng (E | (n + 1)))))) = Integral (M1,((Integral2 (M2,(f | En))) + (Integral2 (M2,(f | En1))))) by A15, A18, A19, A20, A21, A26, A27, Th22;
hence Integral ((Prod_Measure (M1,M2)),(f | (union (rng (E | (n + 1)))))) = Integral (M1,(Integral2 (M2,(f | (union (rng (E | (n + 1)))))))) by A5, A6, A16, A25, Lm12; :: thesis: verum
end;
end;
end;
end;
end;
A28: union (rng E) = dom f by A7, MESFUNC3:def 1;
for n being Nat holds S2[n] from NAT_1:sch 2(A8, A14);
 then Integral ((Prod_Measure (M1,M2)),(f | (union (rng (E | (len E)))))) = Integral (M1,(Integral2 (M2,(f | (union (rng (E | (len E)))))))) ;
then Integral ((Prod_Measure (M1,M2)),(f | (union (rng E)))) = Integral (M1,(Integral2 (M2,(f | (union (rng (E | (len E)))))))) by FINSEQ_1:58;
hence Integral ((Prod_Measure (M1,M2)),f) = Integral (M1,(Integral2 (M2,f))) by A28, FINSEQ_1:58; :: thesis: verum