let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for BSeq, ASeq being SetSequence of Sigma
for B being Event of Sigma st ( for n being Element of NAT holds BSeq . n = (ASeq . n) /\ B ) holds
(Intersection ASeq) /\ B = Intersection BSeq
let Sigma be SigmaField of Omega; :: thesis: for BSeq, ASeq being SetSequence of Sigma
for B being Event of Sigma st ( for n being Element of NAT holds BSeq . n = (ASeq . n) /\ B ) holds
(Intersection ASeq) /\ B = Intersection BSeq
let BSeq, ASeq be SetSequence of Sigma; :: thesis: for B being Event of Sigma st ( for n being Element of NAT holds BSeq . n = (ASeq . n) /\ B ) holds
(Intersection ASeq) /\ B = Intersection BSeq
let B be Event of Sigma; :: thesis: ( ( for n being Element of NAT holds BSeq . n = (ASeq . n) /\ B ) implies (Intersection ASeq) /\ B = Intersection BSeq )
assume A1: for n being Element of NAT holds BSeq . n = (ASeq . n) /\ B ; :: thesis: (Intersection ASeq) /\ B = Intersection BSeq

A2: now

let x be set ; :: 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 Element of NAT holds x in (ASeq . n) /\ B

proof

let n be Element of NAT ; :: thesis: x in (ASeq . n) /\ B
x in BSeq . n by A3, PROB_1:29;
hence x in (ASeq . n) /\ B by A1; :: thesis: verum

end;

A5: for n being Element of NAT holds
( x in ASeq . n & x in B )

proof

let n be Element of 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;

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

end;

now

let x be set ; :: 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 Element of NAT holds x in (ASeq . n) /\ B

proof

let n be Element of NAT ; :: thesis: x in (ASeq . n) /\ B
( x in ASeq . n & x in B ) by A6, A7, PROB_1:29, XBOOLE_0:def 4;
hence x in (ASeq . n) /\ B by XBOOLE_0:def 4; :: thesis: verum

end;

for n being Element of NAT holds x in BSeq . n

proof

let n be Element of NAT ; :: thesis: x in BSeq . n
x in (ASeq . n) /\ B by A8;
hence x in BSeq . n by A1; :: thesis: verum

end;

hence x in Intersection BSeq by PROB_1:29; :: thesis: verum

end;

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