let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for A being SetSequence of Sigma
for n being Nat holds . n = (() . n) `

let Sigma be SigmaField of Omega; :: thesis: for A being SetSequence of Sigma
for n being Nat holds . n = (() . n) `

let A be SetSequence of Sigma; :: thesis: for n being Nat holds . n = (() . n) `
let n be Nat; :: thesis: . n = (() . n) `
for x being object holds
( x in . n iff x in (() . n) ` )
proof
let x be object ; :: thesis: ( x in . n iff x in (() . n) ` )
hereby :: thesis: ( x in (() . n) ` implies x in . n )
assume A1: x in . n ; :: thesis: x in (() . n) `
then A2: x in Intersection (() ^\ 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 (() ^\ n) . k by ;
then x in () . (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 ;
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 ;
A6: not x in () . n by ;
A7: x in Omega \ (() . n) by ;
thus x in (() . n) ` by ; :: thesis: verum
end;
assume A8: x in (() . n) ` ; :: thesis: x in . n
A9: ( x in (() . n) ` iff x in Omega \ (() . n) ) by SUBSET_1:def 4;
A10: ( x in () . n iff x in Union (A ^\ n) ) by Def7;
A11: for k being Nat holds x in (() ^\ n) . k
proof
let k be Nat; :: thesis: x in (() ^\ n) . k
A12: not x in (A ^\ n) . k by ;
A13: not x in A . (n + k) by ;
A14: x in Omega \ (A . (n + k)) by ;
( x in (A . (n + k)) ` iff x in () . (n + k) ) by PROB_1:def 2;
hence x in (() ^\ n) . k by ; :: thesis: verum
end;
x in Intersection (() ^\ n) by ;
hence x in . n by Def9; :: thesis: verum
end;
hence (Intersect_Shift_Seq ()) . n = (() . n) ` by TARSKI:2; :: thesis: verum