:: deftheorem Def2 defines Product-Probability RANDOM_2:def 2 :
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 b₅ being Probability of Trivial-SigmaField [:Omega1,Omega2:] holds
( b₅ = Product-Probability (Omega1,Omega2,P1,P2) iff ex Q being Function of [:Omega1,Omega2:],REAL st
( ( for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds b₅ . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) ) );