let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for A being SetSequence of Sigma
for n being Nat holds (Intersect_Shift_Seq (Complement A)) . n = ((Union_Shift_Seq A) . n) `
let Sigma be SigmaField of Omega; :: thesis: for A being SetSequence of Sigma
for n being Nat holds (Intersect_Shift_Seq (Complement A)) . n = ((Union_Shift_Seq A) . n) `
let A be SetSequence of Sigma; :: thesis: for n being Nat holds (Intersect_Shift_Seq (Complement A)) . n = ((Union_Shift_Seq A) . n) `
let n be Nat; :: thesis: (Intersect_Shift_Seq (Complement A)) . n = ((Union_Shift_Seq A) . n) `
for x being object holds
( x in (Intersect_Shift_Seq (Complement A)) . n iff x in ((Union_Shift_Seq A) . n) ` )

proof

let x be object ; :: thesis: ( x in (Intersect_Shift_Seq (Complement A)) . n iff x in ((Union_Shift_Seq A) . n) ` )

hereby :: thesis: ( x in ((Union_Shift_Seq A) . n) ` implies x in (Intersect_Shift_Seq (Complement A)) . n )

assume A1: x in (Intersect_Shift_Seq (Complement A)) . n ; :: thesis: x in ((Union_Shift_Seq A) . n) `
then A2: x in Intersection ((Complement A) ^\ n) by Def9;
A3: for k being Nat holds not x in (A ^\ n) . k

proof

let k be Nat; :: thesis: not x in (A ^\ n) . k
x in ((Complement A) ^\ n) . k by A2, PROB_1:13;
then x in (Complement A) . (n + k) by NAT_1:def 3;
then A4: x in (A . (n + k)) ` by PROB_1:def 2;
x in Omega \ (A . (n + k)) by A4, SUBSET_1:def 4;
then ( x in Omega & not x in A . (n + k) ) by XBOOLE_0:def 5;
hence not x in (A ^\ n) . k by NAT_1:def 3; :: thesis: verum

end;

A5: not x in Union (A ^\ n) by A3, PROB_1:12;
A6: not x in (Union_Shift_Seq A) . n by Def7, A5;
A7: x in Omega \ ((Union_Shift_Seq A) . n) by A1, A6, XBOOLE_0:def 5;
thus x in ((Union_Shift_Seq A) . n) ` by A7, SUBSET_1:def 4; :: thesis: verum

end;

assume A8: x in ((Union_Shift_Seq A) . n) ` ; :: thesis: x in (Intersect_Shift_Seq (Complement A)) . n
A9: ( x in ((Union_Shift_Seq A) . n) ` iff x in Omega \ ((Union_Shift_Seq A) . n) ) by SUBSET_1:def 4;
A10: ( x in (Union_Shift_Seq A) . n iff x in Union (A ^\ n) ) by Def7;
A11: for k being Nat holds x in ((Complement A) ^\ n) . k

proof

let k be Nat; :: thesis: x in ((Complement A) ^\ n) . k
A12: not x in (A ^\ n) . k by A10, A8, A9, PROB_1:12, XBOOLE_0:def 5;
A13: not x in A . (n + k) by A12, NAT_1:def 3;
A14: x in Omega \ (A . (n + k)) by A8, A13, XBOOLE_0:def 5;
( x in (A . (n + k)) ` iff x in (Complement A) . (n + k) ) by PROB_1:def 2;
hence x in ((Complement A) ^\ n) . k by A14, NAT_1:def 3, SUBSET_1:def 4; :: thesis: verum

end;

x in Intersection ((Complement A) ^\ n) by A11, PROB_1:13;
hence x in (Intersect_Shift_Seq (Complement A)) . n by Def9; :: thesis: verum

end;

hence (Intersect_Shift_Seq (Complement A)) . n = ((Union_Shift_Seq A) . n) ` by TARSKI:2; :: thesis: verum