for Omega being non empty set
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