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 AS: ( ( 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;

A1: now

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 set such that
P11: ( x in Omega1 & y in Omega2 & z = [x,y] ) by ZFMISC_1:def 2;
for xx being set st xx in {x} holds
xx in Omega1 by P11, TARSKI:def 1;
then EXY: ( {x} is Event of Trivial-SigmaField Omega1 & ( for xx being set st xx in {y} holds
xx in Omega2 ) ) by P11, TARSKI:def 1, TARSKI:def 3;
then EXY1: {y} is Event of Trivial-SigmaField Omega2 by TARSKI:def 3;
P12: Q . z = Q . x,y by P11
.= (P1 . {x}) * (P2 . {y}) by P11, AS ;
( 0 <= P1 . {x} & 0 <= P2 . {y} ) by EXY, EXY1, PROB_1:def 13;
hence 0 <= Q . z by P12; :: 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 A1;
then 0 <= setopfunc Y,[:Omega1,Omega2:],REAL ,Q,addreal by LMXY093;
hence 0 <= P . x by AS; :: thesis: P . x <= 1
A12: setopfunc Y,[:Omega1,Omega2:],REAL ,Q,addreal <= setopfunc Y12,[:Omega1,Omega2:],REAL ,Q,addreal by A1, LMXY094;
setopfunc Y12,[:Omega1,Omega2:],REAL ,Q,addreal = P . [:Omega1,Omega2:] by AS;
then setopfunc Y,[:Omega1,Omega2:],REAL ,Q,addreal <= 1 by A12, AS, LMXY10;
hence P . x <= 1 by AS; :: thesis: verum