let Omega be non empty set ; for Sigma being SigmaField of Omega
for X, Y being random_variable of Sigma, Borel_Sets holds X (#) Y is random_variable of Sigma, Borel_Sets
let Sigma be SigmaField of Omega; for X, Y being random_variable of Sigma, Borel_Sets holds X (#) Y is random_variable of Sigma, Borel_Sets
let X, Y be random_variable of Sigma, Borel_Sets ; X (#) Y is random_variable of Sigma, Borel_Sets
reconsider X = X, Y = Y as Real-Valued-Random-Variable of Sigma by RANDOM_3:9;
X (#) Y is Real-Valued-Random-Variable of Sigma
;
hence
X (#) Y is random_variable of Sigma, Borel_Sets
by RANDOM_3:9; verum