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
A2: now :: thesis: for x being object st x in Intersection BSeq holds
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
proof
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;
A5: for n being Nat holds
( x in ASeq . n & x in B )
proof
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;
then x in Intersection ASeq by PROB_1:13;
hence x in (Intersection ASeq) /\ B by A5, XBOOLE_0:def 4; :: thesis: verum
end;
now :: thesis: for x being object st x in (Intersection ASeq) /\ B holds
x 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
proof
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;
for n being Nat holds x in BSeq . n
proof
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;
hence x in Intersection BSeq by PROB_1:13; :: thesis: verum
end;
hence (Intersection ASeq) /\ B = Intersection BSeq by A2, TARSKI:2; :: thesis: verum