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 Q1, Q2 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 x, y being set st x in Omega1 & y in Omega2 holds
Q2 . (x,y) = (P1 . {x}) * (P2 . {y}) ) holds
Q1 = Q2
let P1 be Probability of Trivial-SigmaField Omega1; :: thesis: for P2 being Probability of Trivial-SigmaField Omega2
for Q1, Q2 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 x, y being set st x in Omega1 & y in Omega2 holds
Q2 . (x,y) = (P1 . {x}) * (P2 . {y}) ) holds
Q1 = Q2
let P2 be Probability of Trivial-SigmaField Omega2; :: thesis: for Q1, Q2 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 x, y being set st x in Omega1 & y in Omega2 holds
Q2 . (x,y) = (P1 . {x}) * (P2 . {y}) ) holds
Q1 = Q2
let Q1, Q2 be Function of [:Omega1,Omega2:],REAL; :: thesis: ( ( for x, y being set st x in Omega1 & y in Omega2 holds
Q1 . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for x, y being set st x in Omega1 & y in Omega2 holds
Q2 . (x,y) = (P1 . {x}) * (P2 . {y}) ) implies Q1 = Q2 )
assume A1: ( ( for x, y being set st x in Omega1 & y in Omega2 holds
Q1 . (x,y) = (P1 . {x}) * (P2 . {y}) ) & ( for x, y being set st x in Omega1 & y in Omega2 holds
Q2 . (x,y) = (P1 . {x}) * (P2 . {y}) ) ) ; :: thesis: Q1 = Q2
A2: ( dom Q1 = [:Omega1,Omega2:] & dom Q2 = [:Omega1,Omega2:] ) by FUNCT_2:def 1;

now :: thesis: for z being object st z in dom Q1 holds
Q1 . z = Q2 . z

let z be object ; :: thesis: ( z in dom Q1 implies Q1 . z = Q2 . z )
assume z in dom Q1 ; :: thesis: Q1 . z = Q2 . z
then consider x, y being object such that
A3: ( x in Omega1 & y in Omega2 & z = [x,y] ) by ZFMISC_1:def 2;
thus Q1 . z = Q1 . (x,y) by A3
.= (P1 . {x}) * (P2 . {y}) by A3, A1
.= Q2 . (x,y) by A3, A1
.= Q2 . z by A3 ; :: thesis: verum

end;

hence Q1 = Q2 by A2, FUNCT_1:2; :: thesis: verum