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