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 . ((Partial_Intersection (Complement A)) . n) = 1 - (Prob . ((Partial_Union 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 . ((Partial_Intersection (Complement A)) . n) = 1 - (Prob . ((Partial_Union A) . n))
let Prob be Probability of Sigma; :: thesis: for A being SetSequence of Sigma
for n being Nat holds Prob . ((Partial_Intersection (Complement A)) . n) = 1 - (Prob . ((Partial_Union A) . n))
let A be SetSequence of Sigma; :: thesis: for n being Nat holds Prob . ((Partial_Intersection (Complement A)) . n) = 1 - (Prob . ((Partial_Union A) . n))
let n be Nat; :: thesis: Prob . ((Partial_Intersection (Complement A)) . n) = 1 - (Prob . ((Partial_Union A) . n))
A1: Prob . ((Partial_Intersection (Complement A)) . n) = Prob . (((Partial_Union A) . n) `) by Th7;
Prob . (((Partial_Union A) . n) `) = Prob . (([#] Sigma) \ ((Partial_Union A) . n)) by SUBSET_1:def 4;
hence Prob . ((Partial_Intersection (Complement A)) . n) = 1 - (Prob . ((Partial_Union A) . n)) by A1, PROB_1:32; :: thesis: verum