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

proof

let z be set ; :: 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 set 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 ; :: thesis: verum

end;

then reconsider f = f as Function of [:Omega1,Omega2:],REAL by FUNCT_2:5, A1;
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