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 Element of 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 Element of 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 Element of 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 Element of NAT holds Prob . ((@Intersect_Shift_Seq (@Complement A)) . n) = 1 - (Prob . ((@Union_Shift_Seq A) . n))
let n be Element of 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 5;
hence Prob . ((@Intersect_Shift_Seq (@Complement A)) . n) = 1 - (Prob . ((@Union_Shift_Seq A) . n)) by PROB_1:68, A1; :: thesis: verum