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 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, Def3;
then r (#) f is_integrable_on P2M P by MESFUNC6:102;
then r (#) f is_integrable_on P by Def3;
hence expect (r (#) f),P = Integral (P2M P),(r (#) f) by Def4
.= (R_EAL r) * (Integral (P2M P),f) by A3, MESFUNC6:102
.= r * (expect f,P) by A2, EXTREAL1:13 ;
:: thesis: verum