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 P1, P2 being Function of (bool [:Omega1,Omega2:]),REAL st ( for z being finite Subset of [:Omega1,Omega2:] holds P1 . z = setopfunc z,[:Omega1,Omega2:],REAL ,Q,addreal ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P2 . z = setopfunc z,[:Omega1,Omega2:],REAL ,Q,addreal ) holds
P1 = P2
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 P1, P2 being Function of (bool [:Omega1,Omega2:]),REAL st ( for z being finite Subset of [:Omega1,Omega2:] holds P1 . z = setopfunc z,[:Omega1,Omega2:],REAL ,Q,addreal ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P2 . z = setopfunc z,[:Omega1,Omega2:],REAL ,Q,addreal ) holds
P1 = P2
let P2 be Probability of Trivial-SigmaField Omega2; :: thesis: for Q being Function of [:Omega1,Omega2:],REAL
for P1, P2 being Function of (bool [:Omega1,Omega2:]),REAL st ( for z being finite Subset of [:Omega1,Omega2:] holds P1 . z = setopfunc z,[:Omega1,Omega2:],REAL ,Q,addreal ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P2 . z = setopfunc z,[:Omega1,Omega2:],REAL ,Q,addreal ) holds
P1 = P2
let Q be Function of [:Omega1,Omega2:],REAL ; :: thesis: for P1, P2 being Function of (bool [:Omega1,Omega2:]),REAL st ( for z being finite Subset of [:Omega1,Omega2:] holds P1 . z = setopfunc z,[:Omega1,Omega2:],REAL ,Q,addreal ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P2 . z = setopfunc z,[:Omega1,Omega2:],REAL ,Q,addreal ) holds
P1 = P2
let P1, P2 be Function of (bool [:Omega1,Omega2:]),REAL ; :: thesis: ( ( for z being finite Subset of [:Omega1,Omega2:] holds P1 . z = setopfunc z,[:Omega1,Omega2:],REAL ,Q,addreal ) & ( for z being finite Subset of [:Omega1,Omega2:] holds P2 . z = setopfunc z,[:Omega1,Omega2:],REAL ,Q,addreal ) implies P1 = P2 )
assume AS1: for z being finite Subset of [:Omega1,Omega2:] holds P1 . z = setopfunc z,[:Omega1,Omega2:],REAL ,Q,addreal ; :: thesis: ( ex z being finite Subset of [:Omega1,Omega2:] st not P2 . z = setopfunc z,[:Omega1,Omega2:],REAL ,Q,addreal or P1 = P2 )
assume AS2: for z being finite Subset of [:Omega1,Omega2:] holds P2 . z = setopfunc z,[:Omega1,Omega2:],REAL ,Q,addreal ; :: thesis: P1 = P2

now

let x be set ; :: thesis: ( x in bool [:Omega1,Omega2:] implies P1 . x = P2 . x )
assume x in bool [:Omega1,Omega2:] ; :: thesis: P1 . x = P2 . x
then reconsider z = x as finite Subset of [:Omega1,Omega2:] ;
thus P1 . x = setopfunc z,[:Omega1,Omega2:],REAL ,Q,addreal by AS1
.= P2 . x by AS2 ; :: thesis: verum

end;

hence P1 = P2 by FUNCT_2:18; :: thesis: verum