let X1, X2 be non empty set ; :: thesis: for S1 being SigmaField of X1
for S2 being SigmaField of X2
for F being FinSequence of measurable_rectangles (S1,S2) holds Union F in sigma (measurable_rectangles (S1,S2))
let S1 be SigmaField of X1; :: thesis: for S2 being SigmaField of X2
for F being FinSequence of measurable_rectangles (S1,S2) holds Union F in sigma (measurable_rectangles (S1,S2))
let S2 be SigmaField of X2; :: thesis: for F being FinSequence of measurable_rectangles (S1,S2) holds Union F in sigma (measurable_rectangles (S1,S2))
let F be FinSequence of measurable_rectangles (S1,S2); :: thesis: Union F in sigma (measurable_rectangles (S1,S2))
defpred S₁[ Nat] means ( $1 <= len F implies union (rng (F | $1)) in sigma (measurable_rectangles (S1,S2)) );
A1: S₁[ 0 ] by ZFMISC_1:2, MEASURE1:34;
A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]
assume A4: k + 1 <= len F ; :: thesis: union (rng (F | (k + 1))) in sigma (measurable_rectangles (S1,S2))
then k + 1 in dom F by NAT_1:11, FINSEQ_3:25;
then A6: F . (k + 1) in measurable_rectangles (S1,S2) by FINSEQ_2:11;
A7: measurable_rectangles (S1,S2) c= sigma (measurable_rectangles (S1,S2)) by PROB_1:def 9;
len (F | (k + 1)) = k + 1 by A4, 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 NAT_1:11, 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:39 ;
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 ;
hence union (rng (F | (k + 1))) in sigma (measurable_rectangles (S1,S2)) by A4, A3, NAT_1:13, A6, A7, MEASURE1:34; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
then union (rng (F | (len F))) in sigma (measurable_rectangles (S1,S2)) ;
then union (rng F) in sigma (measurable_rectangles (S1,S2)) by FINSEQ_1:58;
hence Union F in sigma (measurable_rectangles (S1,S2)) by CARD_3:def 4; :: thesis: verum