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 ex Q being Function of [:Omega1,Omega2:],REAL st
for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y})
let P1 be Probability of Trivial-SigmaField Omega1; :: thesis: for P2 being Probability of Trivial-SigmaField Omega2 ex Q being Function of [:Omega1,Omega2:],REAL st
for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y})
let P2 be Probability of Trivial-SigmaField Omega2; :: thesis: ex Q being Function of [:Omega1,Omega2:],REAL st
for x, y being set st x in Omega1 & y in Omega2 holds
Q . (x,y) = (P1 . {x}) * (P2 . {y})
deffunc H₁( object , object ) -> set = (P1 . {$1}) * (P2 . {$2});
consider f being Function such that
A1: ( dom f = [:Omega1,Omega2:] & ( for x, y being object st x in Omega1 & y in Omega2 holds
f . (x,y) = H₁(x,y) ) ) from FUNCT_3:sch 2();
for z being object st z in [:Omega1,Omega2:] holds
f . z in REAL

proof

let z be object ; :: thesis: ( z in [:Omega1,Omega2:] implies f . z in REAL )
assume z in [:Omega1,Omega2:] ; :: thesis: f . z in REAL
then consider x, y being object such that
A2: ( x in Omega1 & y in Omega2 & z = [x,y] ) by ZFMISC_1:def 2;
f . z = f . (x,y) by A2
.= H₁(x,y) by A1, A2 ;
hence f . z in REAL by XREAL_0:def 1; :: thesis: verum

end;

then reconsider f = f as Function of [:Omega1,Omega2:],REAL by A1, FUNCT_2:3;
take f ; :: thesis: for x, y being set st x in Omega1 & y in Omega2 holds
f . (x,y) = (P1 . {x}) * (P2 . {y})
thus for x, y being set st x in Omega1 & y in Omega2 holds
f . (x,y) = (P1 . {x}) * (P2 . {y}) by A1; :: thesis: verum