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 ex P being Function of (bool [:Omega1,Omega2:]),REAL st
for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal)
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 ex P being Function of (bool [:Omega1,Omega2:]),REAL st
for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal)
let P2 be Probability of Trivial-SigmaField Omega2; :: thesis: for Q being Function of [:Omega1,Omega2:],REAL ex P being Function of (bool [:Omega1,Omega2:]),REAL st
for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal)
let Q be Function of [:Omega1,Omega2:],REAL; :: thesis: ex P being Function of (bool [:Omega1,Omega2:]),REAL st
for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal)
defpred S₁[ object , object ] means ex z being finite Subset of [:Omega1,Omega2:] st
( $1 = z & $2 = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) );
A1: for x being object st x in bool [:Omega1,Omega2:] holds
ex y being object st
( y in REAL & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in bool [:Omega1,Omega2:] implies ex y being object st
( y in REAL & S₁[x,y] ) )
assume x in bool [:Omega1,Omega2:] ; :: thesis: ex y being object st
( y in REAL & S₁[x,y] )
then reconsider z = x as finite Subset of [:Omega1,Omega2:] ;
setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) in REAL ;
hence ex y being object st
( y in REAL & S₁[x,y] ) ; :: thesis: verum

end;

consider P being Function of (bool [:Omega1,Omega2:]),REAL such that
A2: for x being object st x in bool [:Omega1,Omega2:] holds
S₁[x,P . x] from FUNCT_2:sch 1(A1);
take P ; :: thesis: for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal)
thus for z being finite Subset of [:Omega1,Omega2:] holds P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) :: thesis: verum

proof

let z be finite Subset of [:Omega1,Omega2:]; :: thesis: P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal)
ex z1 being finite Subset of [:Omega1,Omega2:] st
( z = z1 & P . z = setopfunc (z1,[:Omega1,Omega2:],REAL,Q,addreal) ) by A2;
hence P . z = setopfunc (z,[:Omega1,Omega2:],REAL,Q,addreal) ; :: thesis: verum

end;