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) ` )

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

hence
(Intersect_Shift_Seq (Complement A)) . n = ((Union_Shift_Seq A) . n) `
by TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in (Intersect_Shift_Seq (Complement A)) . n iff x in ((Union_Shift_Seq 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

hence x in (Intersect_Shift_Seq (Complement A)) . n by Def9; :: thesis: verum

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

assume A8:
x in ((Union_Shift_Seq A) . n) `
; :: thesis: x in (Intersect_Shift_Seq (Complement A)) . nassume 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

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;then A2: x in Intersection ((Complement A) ^\ n) by Def9;

A3: for k being Nat holds not x in (A ^\ n) . k

proof

A5:
not x in Union (A ^\ n)
by A3, PROB_1:12;
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;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

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

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

x in Intersection ((Complement A) ^\ n)
by A11, PROB_1:13;
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;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

hence x in (Intersect_Shift_Seq (Complement A)) . n by Def9; :: thesis: verum