let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega

for Prob being Probability of Sigma

for A being SetSequence of Sigma

for n being Nat holds Prob . ((Intersect_Shift_Seq (Complement A)) . n) = 1 - (Prob . ((Union_Shift_Seq A) . n))

let Sigma be SigmaField of Omega; :: thesis: for Prob being Probability of Sigma

for A being SetSequence of Sigma

for n being Nat holds Prob . ((Intersect_Shift_Seq (Complement A)) . n) = 1 - (Prob . ((Union_Shift_Seq A) . n))

let Prob be Probability of Sigma; :: thesis: for A being SetSequence of Sigma

for n being Nat holds Prob . ((Intersect_Shift_Seq (Complement A)) . n) = 1 - (Prob . ((Union_Shift_Seq A) . n))

let A be SetSequence of Sigma; :: thesis: for n being Nat holds Prob . ((Intersect_Shift_Seq (Complement A)) . n) = 1 - (Prob . ((Union_Shift_Seq A) . n))

let n be Nat; :: thesis: Prob . ((Intersect_Shift_Seq (Complement A)) . n) = 1 - (Prob . ((Union_Shift_Seq A) . n))

A1: Prob . ((Intersect_Shift_Seq (Complement A)) . n) = Prob . (((Union_Shift_Seq A) . n) `) by Th9;

Prob . (((Union_Shift_Seq A) . n) `) = Prob . (([#] Sigma) \ ((Union_Shift_Seq A) . n)) by SUBSET_1:def 4;

hence Prob . ((Intersect_Shift_Seq (Complement A)) . n) = 1 - (Prob . ((Union_Shift_Seq A) . n)) by A1, PROB_1:32; :: thesis: verum

for Prob being Probability of Sigma

for A being SetSequence of Sigma

for n being Nat holds Prob . ((Intersect_Shift_Seq (Complement A)) . n) = 1 - (Prob . ((Union_Shift_Seq A) . n))

let Sigma be SigmaField of Omega; :: thesis: for Prob being Probability of Sigma

for A being SetSequence of Sigma

for n being Nat holds Prob . ((Intersect_Shift_Seq (Complement A)) . n) = 1 - (Prob . ((Union_Shift_Seq A) . n))

let Prob be Probability of Sigma; :: thesis: for A being SetSequence of Sigma

for n being Nat holds Prob . ((Intersect_Shift_Seq (Complement A)) . n) = 1 - (Prob . ((Union_Shift_Seq A) . n))

let A be SetSequence of Sigma; :: thesis: for n being Nat holds Prob . ((Intersect_Shift_Seq (Complement A)) . n) = 1 - (Prob . ((Union_Shift_Seq A) . n))

let n be Nat; :: thesis: Prob . ((Intersect_Shift_Seq (Complement A)) . n) = 1 - (Prob . ((Union_Shift_Seq A) . n))

A1: Prob . ((Intersect_Shift_Seq (Complement A)) . n) = Prob . (((Union_Shift_Seq A) . n) `) by Th9;

Prob . (((Union_Shift_Seq A) . n) `) = Prob . (([#] Sigma) \ ((Union_Shift_Seq A) . n)) by SUBSET_1:def 4;

hence Prob . ((Intersect_Shift_Seq (Complement A)) . n) = 1 - (Prob . ((Union_Shift_Seq A) . n)) by A1, PROB_1:32; :: thesis: verum