for Omega being non empty set
for Sigma being SigmaField of Omega
for P being Probability of Sigma
for f, g being Real-Valued-Random-Variable of Sigma st f is_integrable_on P & g is_integrable_on P holds
expect ((f + g),P) = (expect (f,P)) + (expect (g,P))