let Omega be set ; :: thesis: for Sigma being SigmaField of Omega

for ASeq, BSeq being SetSequence of Sigma

for B being Event of Sigma st ( for n being Nat holds BSeq . n = (ASeq . n) /\ B ) holds

(Intersection ASeq) /\ B = Intersection BSeq

let Sigma be SigmaField of Omega; :: thesis: for ASeq, BSeq being SetSequence of Sigma

for B being Event of Sigma st ( for n being Nat holds BSeq . n = (ASeq . n) /\ B ) holds

(Intersection ASeq) /\ B = Intersection BSeq

let ASeq, BSeq be SetSequence of Sigma; :: thesis: for B being Event of Sigma st ( for n being Nat holds BSeq . n = (ASeq . n) /\ B ) holds

(Intersection ASeq) /\ B = Intersection BSeq

let B be Event of Sigma; :: thesis: ( ( for n being Nat holds BSeq . n = (ASeq . n) /\ B ) implies (Intersection ASeq) /\ B = Intersection BSeq )

assume A1: for n being Nat holds BSeq . n = (ASeq . n) /\ B ; :: thesis: (Intersection ASeq) /\ B = Intersection BSeq

for ASeq, BSeq being SetSequence of Sigma

for B being Event of Sigma st ( for n being Nat holds BSeq . n = (ASeq . n) /\ B ) holds

(Intersection ASeq) /\ B = Intersection BSeq

let Sigma be SigmaField of Omega; :: thesis: for ASeq, BSeq being SetSequence of Sigma

for B being Event of Sigma st ( for n being Nat holds BSeq . n = (ASeq . n) /\ B ) holds

(Intersection ASeq) /\ B = Intersection BSeq

let ASeq, BSeq be SetSequence of Sigma; :: thesis: for B being Event of Sigma st ( for n being Nat holds BSeq . n = (ASeq . n) /\ B ) holds

(Intersection ASeq) /\ B = Intersection BSeq

let B be Event of Sigma; :: thesis: ( ( for n being Nat holds BSeq . n = (ASeq . n) /\ B ) implies (Intersection ASeq) /\ B = Intersection BSeq )

assume A1: for n being Nat holds BSeq . n = (ASeq . n) /\ B ; :: thesis: (Intersection ASeq) /\ B = Intersection BSeq

A2: now :: thesis: for x being object st x in Intersection BSeq holds

x in (Intersection ASeq) /\ B

x in (Intersection ASeq) /\ B

let x be object ; :: thesis: ( x in Intersection BSeq implies x in (Intersection ASeq) /\ B )

assume A3: x in Intersection BSeq ; :: thesis: x in (Intersection ASeq) /\ B

A4: for n being Nat holds x in (ASeq . n) /\ B

( x in ASeq . n & x in B )

hence x in (Intersection ASeq) /\ B by A5, XBOOLE_0:def 4; :: thesis: verum

end;assume A3: x in Intersection BSeq ; :: thesis: x in (Intersection ASeq) /\ B

A4: for n being Nat holds x in (ASeq . n) /\ B

proof

A5:
for n being Nat holds
let n be Nat; :: thesis: x in (ASeq . n) /\ B

x in BSeq . n by A3, PROB_1:13;

hence x in (ASeq . n) /\ B by A1; :: thesis: verum

end;x in BSeq . n by A3, PROB_1:13;

hence x in (ASeq . n) /\ B by A1; :: thesis: verum

( x in ASeq . n & x in B )

proof

then
x in Intersection ASeq
by PROB_1:13;
let n be Nat; :: thesis: ( x in ASeq . n & x in B )

x in (ASeq . n) /\ B by A4;

hence ( x in ASeq . n & x in B ) by XBOOLE_0:def 4; :: thesis: verum

end;x in (ASeq . n) /\ B by A4;

hence ( x in ASeq . n & x in B ) by XBOOLE_0:def 4; :: thesis: verum

hence x in (Intersection ASeq) /\ B by A5, XBOOLE_0:def 4; :: thesis: verum

now :: thesis: for x being object st x in (Intersection ASeq) /\ B holds

x in Intersection BSeq

hence
(Intersection ASeq) /\ B = Intersection BSeq
by A2, TARSKI:2; :: thesis: verumx in Intersection BSeq

let x be object ; :: thesis: ( x in (Intersection ASeq) /\ B implies x in Intersection BSeq )

assume A6: x in (Intersection ASeq) /\ B ; :: thesis: x in Intersection BSeq

then A7: x in Intersection ASeq by XBOOLE_0:def 4;

A8: for n being Nat holds x in (ASeq . n) /\ B

end;assume A6: x in (Intersection ASeq) /\ B ; :: thesis: x in Intersection BSeq

then A7: x in Intersection ASeq by XBOOLE_0:def 4;

A8: for n being Nat holds x in (ASeq . n) /\ B

proof

for n being Nat holds x in BSeq . n
let n be Nat; :: thesis: x in (ASeq . n) /\ B

( x in ASeq . n & x in B ) by A6, A7, PROB_1:13, XBOOLE_0:def 4;

hence x in (ASeq . n) /\ B by XBOOLE_0:def 4; :: thesis: verum

end;( x in ASeq . n & x in B ) by A6, A7, PROB_1:13, XBOOLE_0:def 4;

hence x in (ASeq . n) /\ B by XBOOLE_0:def 4; :: thesis: verum

proof

hence
x in Intersection BSeq
by PROB_1:13; :: thesis: verum
let n be Nat; :: thesis: x in BSeq . n

x in (ASeq . n) /\ B by A8;

hence x in BSeq . n by A1; :: thesis: verum

end;x in (ASeq . n) /\ B by A8;

hence x in BSeq . n by A1; :: thesis: verum