theorem Th21: :: RANDOM_3:21

for D being non-empty finite-yielding ManySortedSet of NAT
for P being Probability_sequence of Trivial-SigmaField_sequence D
for n being Nat ex Pn being Probability of Trivial-SigmaField ((Product_dom D) . n) st
( Pn = (Product-Probability (P,D)) . n & (Product-Probability (P,D)) . (n + 1) = Product-Probability (((Product_dom D) . n),(D . (n + 1)),Pn,(P . (n + 1))) )