consider Q being Function of [:Omega1,Omega2:],REAL such that
P1: for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) by LMXY04;
consider P being Function of (bool [:Omega1,Omega2:]),REAL such that
P2: for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) by LMXY07;
P3: for x being set st x c= [:Omega1,Omega2:] holds
( 0 <= P . x & P . x <= 1 ) by LMXY09, P1, P2;
P . [:Omega1,Omega2:] = 1 by P1, P2, LMXY10;
then P is Probability of Trivial-SigmaField [:Omega1,Omega2:] by P2, P3, LMXY03;
hence ex b₁ being Probability of Trivial-SigmaField [:Omega1,Omega2:] 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) ) ) by P1, P2; :: thesis: verum