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 A4: 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 A5: 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
A6: ( ( 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 A4;
consider Q2 being Function of [:Omega1,Omega2:],REAL such that
A7: ( ( 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 A5;
Q1 = Q2 by A6, A7, Lm2;
hence PP1 = PP2 by Lm4, A6, A7; :: thesis: verum