:: deftheorem Def13 defines Product-Probability RANDOM_3:def 13 :
for D being non-empty finite-yielding ManySortedSet of NAT
for P being Probability_sequence of Trivial-SigmaField_sequence D
for b₃ being ManySortedSet of NAT holds
( b₃ = Product-Probability (P,D) iff ( b₃ . 0 = P . 0 & ( for i being Nat holds b₃ . (i + 1) = Product-Probability (((Product_dom D) . i),(D . (i + 1)),(modetrans ((b₃ . i),(Trivial-SigmaField ((Product_dom D) . i)))),(P . (i + 1))) ) ) );