theorem Th16: :: RANDOM_2:16

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 being non empty finite Subset of Omega1
for Y2 being non empty finite Subset of Omega2 holds (Product-Probability (Omega1,Omega2,P1,P2)) . [:Y1,Y2:] = (P1 . Y1) * (P2 . Y2)