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 A1: 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 A2: for z being finite Subset of [:Omega1,Omega2:] holds P2 . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ; :: thesis: P1 = P2
now :: thesis: for x being object st x in bool [:Omega1,Omega2:] holds
P1 . x = P2 . x
let x be object ; :: 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 A1
.= P2 . x by A2 ; :: thesis: verum
end;
hence P1 = P2 by FUNCT_2:12; :: thesis: verum