let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for A being SetSequence of Sigma
for n being Element of 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 Element of NAT holds (@Intersect_Shift_Seq (@Complement A)) . n = ((@Union_Shift_Seq A) . n) `
let A be SetSequence of Sigma; :: thesis: for n being Element of NAT holds (@Intersect_Shift_Seq (@Complement A)) . n = ((@Union_Shift_Seq A) . n) `
let n be Element of NAT ; :: thesis: (@Intersect_Shift_Seq (@Complement A)) . n = ((@Union_Shift_Seq A) . n) `
for x being set holds
( x in (@Intersect_Shift_Seq (@Complement A)) . n iff x in ((@Union_Shift_Seq A) . n) ` )

proof

let x be set ; :: 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 (Shift_Seq ((@Complement A),n)) by Def12;
A3: for k being Element of NAT holds not x in (@Shift_Seq (A,n)) . k

proof

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

end;

A5: not x in Union (@Shift_Seq (A,n)) by A3, PROB_1:25;
A6: not x in (@Union_Shift_Seq A) . n by Def9, 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 SUBSET_1:def 5, A7; :: 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 5;
A10: ( x in (@Union_Shift_Seq A) . n iff x in Union (@Shift_Seq (A,n)) ) by Def9;
A11: for k being Element of NAT holds x in (@Shift_Seq ((@Complement A),n)) . k

proof

let k be Element of NAT ; :: thesis: x in (@Shift_Seq ((@Complement A),n)) . k
A12: not x in (@Shift_Seq (A,n)) . k by A10, A8, A9, XBOOLE_0:def 5, PROB_1:25;
A13: not x in A . (n + k) by NAT_1:def 3, A12;
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 4;
hence x in (@Shift_Seq ((@Complement A),n)) . k by A14, SUBSET_1:def 5, NAT_1:def 3; :: thesis: verum

end;

x in Intersection (@Shift_Seq ((@Complement A),n)) by A11, PROB_1:29;
hence x in (@Intersect_Shift_Seq (@Complement A)) . n by Def12; :: thesis: verum

end;

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