let Omega be non empty set ; :: thesis: for r being Real
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for f being Real-Valued-Random-Variable of Sigma st f is_integrable_on P holds
expect (r (#) f),P = r * (expect f,P)
let r be Real; :: thesis: for Sigma being SigmaField of Omega
for P being Probability of Sigma
for f being Real-Valued-Random-Variable of Sigma 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 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 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: ( f is_integrable_on P implies expect (r (#) f),P = r * (expect f,P) )
set h = r (#) f;
assume AS0: f is_integrable_on P ; :: thesis: expect (r (#) f),P = r * (expect f,P)
then AS: f is_integrable_on P2M P by defintf;
P7: Integral (P2M P),f = expect f,P by AS0, def2;
r (#) f is_integrable_on P2M P by AS, MESFUNC6:102;
then r (#) f is_integrable_on P by defintf;
hence expect (r (#) f),P = Integral (P2M P),(r (#) f) by def2
.= (R_EAL r) * (Integral (P2M P),f) by AS, MESFUNC6:102
.= r * (expect f,P) by P7, EXTREAL1:13 ;
:: thesis: verum