let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for f being Real-Valued-Random-Variable of Sigma
for r being Real st f is_integrable_on P holds
expect ((r (#) f),P) = r * (expect (f,P))
let Sigma be SigmaField of Omega; :: thesis: for P being Probability of Sigma
for f being Real-Valued-Random-Variable of Sigma
for r being Real st f is_integrable_on P holds
expect ((r (#) f),P) = r * (expect (f,P))
let P be Probability of Sigma; :: thesis: for f being Real-Valued-Random-Variable of Sigma
for r being Real st f is_integrable_on P holds
expect ((r (#) f),P) = r * (expect (f,P))
let f be Real-Valued-Random-Variable of Sigma; :: thesis: for r being Real st f is_integrable_on P holds
expect ((r (#) f),P) = r * (expect (f,P))
let r be Real; :: thesis: ( f is_integrable_on P implies expect ((r (#) f),P) = r * (expect (f,P)) )
set h = r (#) f;
assume A1: f is_integrable_on P ; :: thesis: expect ((r (#) f),P) = r * (expect (f,P))
then A2: Integral ((P2M P),f) = expect (f,P) by Def4;
A3: f is_integrable_on P2M P by A1;
then r (#) f is_integrable_on P2M P by MESFUNC6:102;
then r (#) f is_integrable_on P ;
hence expect ((r (#) f),P) = Integral ((P2M P),(r (#) f)) by Def4
.= r * (Integral ((P2M P),f)) by A3, MESFUNC6:102
.= r * (expect (f,P)) by A2, EXTREAL1:1 ;
:: thesis: verum