theorem Th6: :: BOR_CANT:6

for Omega being non empty set
for Sigma being SigmaField of Omega
for Prob being Probability of Sigma
for A being SetSequence of Sigma
for n, n1, n2 being Nat st n > n1 & A is_all_independent_wrt Prob holds
Prob . (((Partial_Intersection (Complement A)) . n1) /\ ((Partial_Intersection (A ^\ ((n1 + n2) + 1))) . ((n - n1) - 1))) = ((Partial_Product (Prob * (Complement A))) . n1) * ((Partial_Product (Prob * (A ^\ ((n1 + n2) + 1)))) . ((n - n1) - 1))