let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for f being Real-Valued-Random-Variable of Sigma
for r being Real holds r (#) f is Real-Valued-Random-Variable of Sigma
let Sigma be SigmaField of Omega; :: thesis: for f being Real-Valued-Random-Variable of Sigma
for r being Real holds r (#) f is Real-Valued-Random-Variable of Sigma
let f be Real-Valued-Random-Variable of Sigma; :: thesis: for r being Real holds r (#) f is Real-Valued-Random-Variable of Sigma
let r be Real; :: thesis: r (#) f is Real-Valued-Random-Variable of Sigma
consider X being Element of Sigma such that
A1: X = Omega and
A2: f is_measurable_on X by Def2;
dom f = X by A1, FUNCT_2:def 1;
hence r (#) f is Real-Valued-Random-Variable of Sigma by A1, A2, Def2, MESFUNC6:21; :: thesis: verum