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 disjoint_valued 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)) . (Union F) = Integral (M2,(X-vol ((Union F),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 disjoint_valued 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)) . (Union F) = Integral (M2,(X-vol ((Union F),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 disjoint_valued 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)) . (Union F) = Integral (M2,(X-vol ((Union F),M1)))
let M1 be sigma_Measure of S1; :: thesis: for M2 being sigma_Measure of S2
for F being disjoint_valued 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)) . (Union F) = Integral (M2,(X-vol ((Union F),M1)))
let M2 be sigma_Measure of S2; :: thesis: for F being disjoint_valued 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)) . (Union F) = Integral (M2,(X-vol ((Union F),M1)))
let F be disjoint_valued 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)) . (Union F) = Integral (M2,(X-vol ((Union F),M1)))
let n be Nat; :: thesis: ( M1 is sigma_finite & F is FinSequence of measurable_rectangles (S1,S2) implies (product_sigma_Measure (M1,M2)) . (Union F) = Integral (M2,(X-vol ((Union F),M1))) )
assume that
A1: M1 is sigma_finite and
A2: F is FinSequence of measurable_rectangles (S1,S2) ; :: thesis: (product_sigma_Measure (M1,M2)) . (Union F) = Integral (M2,(X-vol ((Union F),M1)))
A3: F | (len F) = F by FINSEQ_1:58;
defpred S₁[ Nat] means (product_sigma_Measure (M1,M2)) . (Union (F | $1)) = Integral (M2,(X-vol ((Union (F | $1)),M1)));
union (rng (F | 0)) = {} by ZFMISC_1:2;
then A4: Union (F | 0) = {} by CARD_3:def 4;
not 0 in dom F by FINSEQ_3:24;
then F . 0 = {} by FUNCT_1:def 2;
then P1: S₁[ 0 ] by A4, A1, A2, Th100;
P2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume P3: S₁[k] ; :: thesis: S₁[k + 1]
A6: k <= k + 1 by NAT_1:13;

per cases ( len F >= k + 1 or len F < k + 1 ) ;

suppose len F >= k + 1 ; :: thesis: S₁[k + 1]

then len (F | (k + 1)) = k + 1 by FINSEQ_1:59;
then F | (k + 1) = ((F | (k + 1)) | k) ^ <*((F | (k + 1)) . (k + 1))*> by FINSEQ_3:55
.= (F | k) ^ <*((F | (k + 1)) . (k + 1))*> by A6, FINSEQ_1:82
.= (F | k) ^ <*(F . (k + 1))*> by FINSEQ_3:112 ;
then rng (F | (k + 1)) = (rng (F | k)) \/ (rng <*(F . (k + 1))*>) by FINSEQ_1:31
.= (rng (F | k)) \/ {(F . (k + 1))} by FINSEQ_1:38 ;
then union (rng (F | (k + 1))) = (union (rng (F | k))) \/ (union {(F . (k + 1))}) by ZFMISC_1:78
.= (union (rng (F | k))) \/ (F . (k + 1)) by ZFMISC_1:25
.= (Union (F | k)) \/ (F . (k + 1)) by CARD_3:def 4 ;
then A8: Union (F | (k + 1)) = (Union (F | k)) \/ (F . (k + 1)) by CARD_3:def 4;
then (product_sigma_Measure (M1,M2)) . (Union (F | (k + 1))) = ((product_sigma_Measure (M1,M2)) . (Union (F | k))) + ((product_sigma_Measure (M1,M2)) . (F . (k + 1))) by Th101, Th12
.= (Integral (M2,(X-vol ((Union (F | k)),M1)))) + (Integral (M2,(X-vol ((F . (k + 1)),M1)))) by A1, A2, P3, Th100 ;
hence S₁[k + 1] by A1, A8, Th101, Th95; :: thesis: verum

end;

suppose len F < k + 1 ; :: thesis: S₁[k + 1]

then ( F | (k + 1) = F & F | k = F ) by FINSEQ_3:49, NAT_1:13;
hence S₁[k + 1] by P3; :: thesis: verum

end;

end;

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(P1, P2);
hence (product_sigma_Measure (M1,M2)) . (Union F) = Integral (M2,(X-vol ((Union F),M1))) by A3; :: thesis: verum