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