theorem :: RANDOM_1:28
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))