let Omega1, Omega2 be non empty finite set ; :: thesis:
let P1 be Probability of Trivial-SigmaField Omega1; :: thesis:
let P2 be Probability of Trivial-SigmaField Omega2; :: thesis:
deffunc H₁( object , object ) -> Element of ExtREAL = (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

let z be object ; :: thesis:
assume z in [:Omega1,Omega2:] ; :: thesis:
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:

end;

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