let PP1, PP2 be Probability of Trivial-SigmaField [:Omega1,Omega2:]; :: thesis: ( 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 PP1 . z = setopfunc z,[:Omega1,Omega2:],REAL ,Q,addreal ) ) & 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 PP2 . z = setopfunc z,[:Omega1,Omega2:],REAL ,Q,addreal ) ) implies PP1 = PP2 )
assume A1: ex Q1 being Function of [:Omega1,Omega2:],REAL st
( ( for x, y being set st x in Omega1 & y in Omega2 holds
Q1 . x,y = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds PP1 . z = setopfunc z,[:Omega1,Omega2:],REAL ,Q1,addreal ) ) ; :: thesis: ( for Q being Function of [:Omega1,Omega2:],REAL holds
( ex x, y being set st
( x in Omega1 & y in Omega2 & not Q . x,y = (P1 . {x}) * (P2 . {y}) ) or ex z being finite Subset of [:Omega1,Omega2:] st not PP2 . z = setopfunc z,[:Omega1,Omega2:],REAL ,Q,addreal ) or PP1 = PP2 )
assume A2: ex Q2 being Function of [:Omega1,Omega2:],REAL st
( ( for x, y being set st x in Omega1 & y in Omega2 holds
Q2 . x,y = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds PP2 . z = setopfunc z,[:Omega1,Omega2:],REAL ,Q2,addreal ) ) ; :: thesis: PP1 = PP2
consider Q1 being Function of [:Omega1,Omega2:],REAL such that
A11: ( ( for x, y being set st x in Omega1 & y in Omega2 holds
Q1 . x,y = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds PP1 . z = setopfunc z,[:Omega1,Omega2:],REAL ,Q1,addreal ) ) by A1;
consider Q2 being Function of [:Omega1,Omega2:],REAL such that
A12: ( ( for x, y being set st x in Omega1 & y in Omega2 holds
Q2 . x,y = (P1 . {x}) * (P2 . {y}) ) & ( for z being finite Subset of [:Omega1,Omega2:] holds PP2 . z = setopfunc z,[:Omega1,Omega2:],REAL ,Q2,addreal ) ) by A2;
Q1 = Q2 by A11, A12, LMXY05;
hence PP1 = PP2 by LMXY08, A11, A12; :: thesis: verum