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 M2 is sigma_finite & F is FinSequence of measurable_rectangles (S1,S2) holds
(product_sigma_Measure (M1,M2)) . (F . n) = Integral (M1,(Y-vol ((F . n),M2)))
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 M2 is sigma_finite & F is FinSequence of measurable_rectangles (S1,S2) holds
(product_sigma_Measure (M1,M2)) . (F . n) = Integral (M1,(Y-vol ((F . n),M2)))
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 M2 is sigma_finite & F is FinSequence of measurable_rectangles (S1,S2) holds
(product_sigma_Measure (M1,M2)) . (F . n) = Integral (M1,(Y-vol ((F . n),M2)))
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 M2 is sigma_finite & F is FinSequence of measurable_rectangles (S1,S2) holds
(product_sigma_Measure (M1,M2)) . (F . n) = Integral (M1,(Y-vol ((F . n),M2)))
let M2 be sigma_Measure of S2; :: thesis: for F being FinSequence of sigma (measurable_rectangles (S1,S2))
for n being Nat st M2 is sigma_finite & F is FinSequence of measurable_rectangles (S1,S2) holds
(product_sigma_Measure (M1,M2)) . (F . n) = Integral (M1,(Y-vol ((F . n),M2)))
let F be FinSequence of sigma (measurable_rectangles (S1,S2)); :: thesis: for n being Nat st M2 is sigma_finite & F is FinSequence of measurable_rectangles (S1,S2) holds
(product_sigma_Measure (M1,M2)) . (F . n) = Integral (M1,(Y-vol ((F . n),M2)))
let n be Nat; :: thesis: ( M2 is sigma_finite & F is FinSequence of measurable_rectangles (S1,S2) implies (product_sigma_Measure (M1,M2)) . (F . n) = Integral (M1,(Y-vol ((F . n),M2))) )
assume that
A1: M2 is sigma_finite and
A2: F is FinSequence of measurable_rectangles (S1,S2) ; :: thesis: (product_sigma_Measure (M1,M2)) . (F . n) = Integral (M1,(Y-vol ((F . n),M2)))
reconsider XX1 = X1 as Element of S1 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 ( ( M1 . P = 0 & M2 . Q = +infty ) or ( M1 . P = 0 & M2 . Q <> +infty ) or ( M1 . P <> 0 & M2 . Q = +infty ) or ( M1 . P <> 0 & M2 . Q <> +infty ) ) ;

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

then ( (product_sigma_Measure (M1,M2)) . (F . n) = 0 & Y-vol ((F . n),M2) = Xchi (P,X1) ) by A1, d4, d5, Th96;
hence (product_sigma_Measure (M1,M2)) . (F . n) = Integral (M1,(Y-vol ((F . n),M2))) by d8, MEASUR10:33; :: thesis: verum

end;

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

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

end;

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

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

end;

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

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

end;

end;