let Omega be non empty set ; :: thesis: 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; :: thesis: 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 ; :: thesis: 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; :: thesis: verum