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 FinSequence of sigma (measurable_rectangles (S1,S2))
for n being Nat st M1 is sigma_finite & F is FinSequence of measurable_rectangles (S1,S2) holds
(product_sigma_Measure (M1,M2)) . (F . n) = Integral (M2,(X-vol ((F . n),M1)))
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 FinSequence of sigma (measurable_rectangles (S1,S2))
for n being Nat st M1 is sigma_finite & F is FinSequence of measurable_rectangles (S1,S2) holds
(product_sigma_Measure (M1,M2)) . (F . n) = Integral (M2,(X-vol ((F . n),M1)))
let S2 be SigmaField of X2; :: thesis: for M1 being sigma_Measure of S1
for M2 being sigma_Measure of S2
for F being FinSequence of sigma (measurable_rectangles (S1,S2))
for n being Nat st M1 is sigma_finite & F is FinSequence of measurable_rectangles (S1,S2) holds
(product_sigma_Measure (M1,M2)) . (F . n) = Integral (M2,(X-vol ((F . n),M1)))
let M1 be sigma_Measure of S1; :: thesis: for M2 being sigma_Measure of S2
for F being FinSequence of sigma (measurable_rectangles (S1,S2))
for n being Nat st M1 is sigma_finite & F is FinSequence of measurable_rectangles (S1,S2) holds
(product_sigma_Measure (M1,M2)) . (F . n) = Integral (M2,(X-vol ((F . n),M1)))
let M2 be sigma_Measure of S2; :: thesis: for F being FinSequence of sigma (measurable_rectangles (S1,S2))
for n being Nat st M1 is sigma_finite & F is FinSequence of measurable_rectangles (S1,S2) holds
(product_sigma_Measure (M1,M2)) . (F . n) = Integral (M2,(X-vol ((F . n),M1)))
let F be FinSequence of sigma (measurable_rectangles (S1,S2)); :: thesis: for n being Nat st M1 is sigma_finite & F is FinSequence of measurable_rectangles (S1,S2) holds
(product_sigma_Measure (M1,M2)) . (F . n) = Integral (M2,(X-vol ((F . n),M1)))
let n be Nat; :: thesis: ( M1 is sigma_finite & F is FinSequence of measurable_rectangles (S1,S2) implies (product_sigma_Measure (M1,M2)) . (F . n) = Integral (M2,(X-vol ((F . n),M1))) )
assume that
A1: M1 is sigma_finite and
A2: F is FinSequence of measurable_rectangles (S1,S2) ; :: thesis: (product_sigma_Measure (M1,M2)) . (F . n) = Integral (M2,(X-vol ((F . n),M1)))
reconsider XX2 = X2 as Element of S2 by MEASURE1:7;
( not n in dom F implies F . n in measurable_rectangles (S1,S2) )

proof

assume not n in dom F ; :: thesis: F . n in measurable_rectangles (S1,S2)
then F . n = {} by FUNCT_1:def 2;
hence F . n in measurable_rectangles (S1,S2) by SETFAM_1:def 8; :: thesis: verum

end;

then F . n in measurable_rectangles (S1,S2) by A2, PARTFUN1:4;
then F . n in { [:A,B:] where A is Element of S1, B is Element of S2 : verum } by MEASUR10:def 5;
then consider P being Element of S1, Q being Element of S2 such that
d4: F . n = [:P,Q:] ;
d5: (product_sigma_Measure (M1,M2)) . (F . n) = (M1 . P) * (M2 . Q) by d4, Th10;

per cases ( ( M2 . Q = 0 & M1 . P = +infty ) or ( M2 . Q = 0 & M1 . P <> +infty ) or ( M2 . Q <> 0 & M1 . P = +infty ) or ( M2 . Q <> 0 & M1 . P <> +infty ) ) ;

suppose d8: ( M2 . Q = 0 & M1 . P = +infty ) ; :: thesis: (product_sigma_Measure (M1,M2)) . (F . n) = Integral (M2,(X-vol ((F . n),M1)))

then ( (product_sigma_Measure (M1,M2)) . (F . n) = 0 & X-vol ((F . n),M1) = Xchi (Q,X2) ) by A1, d4, d5, Th97;
hence (product_sigma_Measure (M1,M2)) . (F . n) = Integral (M2,(X-vol ((F . n),M1))) by d8, MEASUR10:33; :: thesis: verum

end;

suppose ( M2 . Q = 0 & M1 . P <> +infty ) ; :: thesis: (product_sigma_Measure (M1,M2)) . (F . n) = Integral (M2,(X-vol ((F . n),M1)))

then ex r being Real st
( r = M1 . P & X-vol ((F . n),M1) = r (#) (chi (Q,X2)) ) by A1, d4, Th97;
hence (product_sigma_Measure (M1,M2)) . (F . n) = Integral (M2,(X-vol ((F . n),M1))) by d5, Th98, SUPINF_2:51; :: thesis: verum

end;

suppose d6: ( M2 . Q <> 0 & M1 . P = +infty ) ; :: thesis: (product_sigma_Measure (M1,M2)) . (F . n) = Integral (M2,(X-vol ((F . n),M1)))

M2 . Q >= 0 by SUPINF_2:51;
then d7: (product_sigma_Measure (M1,M2)) . (F . n) = +infty by d5, d6, XXREAL_3:def 5;
X-vol ((F . n),M1) = Xchi (Q,X2) by A1, d4, d6, Th97;
hence (product_sigma_Measure (M1,M2)) . (F . n) = Integral (M2,(X-vol ((F . n),M1))) by d7, d6, MEASUR10:33; :: thesis: verum

end;

suppose ( M2 . Q <> 0 & M1 . P <> +infty ) ; :: thesis: (product_sigma_Measure (M1,M2)) . (F . n) = Integral (M2,(X-vol ((F . n),M1)))

then ex r being Real st
( r = M1 . P & X-vol ((F . n),M1) = r (#) (chi (Q,X2)) ) by A1, d4, Th97;
hence (product_sigma_Measure (M1,M2)) . (F . n) = Integral (M2,(X-vol ((F . n),M1))) by d5, Th98, SUPINF_2:51; :: thesis: verum

end;

end;