consider Q being Function of [:Omega1,Omega2:],REAL such that
A1: for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y}) by Lm1;
consider P being Function of (bool [:Omega1,Omega2:]),REAL such that
A2: for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) by Lm3;
A3: for x being set st x c= [:Omega1,Omega2:] holds
( 0 <= P . x & P . x <= 1 ) by Lm9, A1, A2;
P . [:Omega1,Omega2:] = 1 by A1, A2, Lm8;
then P is Probability of Trivial-SigmaField [:Omega1,Omega2:] by A2, A3, Th8;
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 A1, A2; :: thesis: verum