:: deftheorem Def4 defines expect RANDOM_1:def 3 :
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 st f is_integrable_on P holds
expect (f,P) = Integral ((P2M P),f);