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₁[ set , set ] means ex z being finite Subset of [:Omega1,Omega2:] st
( $1 = z & $2 = setopfunc z,[:Omega1,Omega2:],REAL ,Q,addreal );
LP1: for x being set st x in bool [:Omega1,Omega2:] holds
ex y being set st
( y in REAL & S₁[x,y] )

proof

let x be set ; :: thesis: ( x in bool [:Omega1,Omega2:] implies ex y being set st
( y in REAL & S₁[x,y] ) )
assume x in bool [:Omega1,Omega2:] ; :: thesis: ex y being set 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 set st
( y in REAL & S₁[x,y] ) ; :: thesis: verum

end;

consider P being Function of (bool [:Omega1,Omega2:]),REAL such that
LP2: for x being set st x in bool [:Omega1,Omega2:] holds
S₁[x,P . x] from FUNCT_2:sch 1(LP1);
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 LP2;
hence P . z = setopfunc z,[:Omega1,Omega2:],REAL ,Q,addreal ; :: thesis: verum

end;