theorem Th20: :: RANDOM_3:20

for D being non-empty finite-yielding ManySortedSet of NAT
for P being Probability_sequence of Trivial-SigmaField_sequence D
for n being Nat holds (Product-Probability (P,D)) . n is Probability of Trivial-SigmaField ((Product_dom D) . n)