theorem :: RANDOM_2:17

for Omega1, Omega2 being non empty finite set
for P1 being Probability of Trivial-SigmaField Omega1
for P2 being Probability of Trivial-SigmaField Omega2
for y1, y2 being set st y1 in Omega1 & y2 in Omega2 holds
(Product-Probability (Omega1,Omega2,P1,P2)) . {[y1,y2]} = (P1 . {y1}) * (P2 . {y2})