let Omega1, Omega2 be non empty finite set ; :: thesis: for P1 being Probability of Trivial-SigmaField Omega1
for P2 being Probability of Trivial-SigmaField Omega2
for Q being Function of [:Omega1,Omega2:],REAL
for P being Function of (bool [: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 P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) holds
for x being set st x c= [:Omega1,Omega2:] holds
( 0 <= P . x & P . x <= 1 )
let P1 be Probability of Trivial-SigmaField Omega1; :: thesis: for P2 being Probability of Trivial-SigmaField Omega2
for Q being Function of [:Omega1,Omega2:],REAL
for P being Function of (bool [: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 P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) holds
for x being set st x c= [:Omega1,Omega2:] holds
( 0 <= P . x & P . x <= 1 )
let P2 be Probability of Trivial-SigmaField Omega2; :: thesis: for Q being Function of [:Omega1,Omega2:],REAL
for P being Function of (bool [: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 P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) holds
for x being set st x c= [:Omega1,Omega2:] holds
( 0 <= P . x & P . x <= 1 )
let Q be Function of [:Omega1,Omega2:],REAL; :: thesis: for P being Function of (bool [: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 P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) holds
for x being set st x c= [:Omega1,Omega2:] holds
( 0 <= P . x & P . x <= 1 )
let P be Function of (bool [:Omega1,Omega2:]),REAL; :: thesis: ( ( 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 P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) implies for x being set st x c= [:Omega1,Omega2:] holds
( 0 <= P . x & P . x <= 1 ) )
assume A1: ( ( 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 P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ) ) ; :: thesis: for x being set st x c= [:Omega1,Omega2:] holds
( 0 <= P . x & P . x <= 1 )
reconsider Y12 = [:Omega1,Omega2:] as finite Subset of [:Omega1,Omega2:] by SUBSET:3;

A2: now :: thesis: for z being set st z in [:Omega1,Omega2:] holds
0 <= Q . z

let z be set ; :: thesis: ( z in [:Omega1,Omega2:] implies 0 <= Q . z )
assume z in [:Omega1,Omega2:] ; :: thesis: 0 <= Q . z
then consider x, y being object such that
A3: ( x in Omega1 & y in Omega2 & z = [x,y] ) by ZFMISC_1:def 2;
for xx being object st xx in {x} holds
xx in Omega1 by A3, TARSKI:def 1;
then A4: ( {x} is Event of Trivial-SigmaField Omega1 & ( for xx being object st xx in {y} holds
xx in Omega2 ) ) by A3, TARSKI:def 1, TARSKI:def 3;
then A5: {y} is Event of Trivial-SigmaField Omega2 by TARSKI:def 3;
A6: Q . z = Q . (x,y) by A3
.= (P1 . {x}) * (P2 . {y}) by A3, A1 ;
( 0 <= P1 . {x} & 0 <= P2 . {y} ) by A4, A5, PROB_1:def 8;
hence 0 <= Q . z by A6; :: thesis: verum

end;

let x be set ; :: thesis: ( x c= [:Omega1,Omega2:] implies ( 0 <= P . x & P . x <= 1 ) )
assume x c= [:Omega1,Omega2:] ; :: thesis: ( 0 <= P . x & P . x <= 1 )
then reconsider Y = x as finite Subset of [:Omega1,Omega2:] ;
for z being set st z in Y holds
0 <= Q . z by A2;
then 0 <= setopfunc (Y,[:Omega1,Omega2:],REAL,Q,addreal) by Th13;
hence 0 <= P . x by A1; :: thesis: P . x <= 1
A7: setopfunc (Y,[:Omega1,Omega2:],REAL,Q,addreal) <= setopfunc (Y12,[:Omega1,Omega2:],REAL,Q,addreal) by A2, Th14;
setopfunc (Y12,[:Omega1,Omega2:],REAL,Q,addreal) = P . [:Omega1,Omega2:] by A1;
then setopfunc (Y,[:Omega1,Omega2:],REAL,Q,addreal) <= 1 by A7, A1, Lm8;
hence P . x <= 1 by A1; :: thesis: verum