let Omega be non empty set ; :: thesis: 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))
let Sigma be SigmaField of Omega; :: thesis: 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))
let P be Probability of Sigma; :: thesis: 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))
let f, g be Real-Valued-Random-Variable of Sigma; :: thesis: ( f is_integrable_on P & g is_integrable_on P implies expect ((f - g),P) = (expect (f,P)) - (expect (g,P)) )
assume that
A1: f is_integrable_on P and
A2: g is_integrable_on P ; :: thesis: expect ((f - g),P) = (expect (f,P)) - (expect (g,P))
g is_integrable_on P2M P by A2;
then (- 1) (#) g is_integrable_on P2M P by MESFUNC6:102;
then (- jj) (#) g is_integrable_on P ;
hence expect ((f - g),P) = (expect (f,P)) + (expect (((- jj) (#) g),P)) by A1, Th26
.= (expect (f,P)) + ((- 1) * (expect (g,P))) by A2, Th27
.= (expect (f,P)) - (expect (g,P)) ;
:: thesis: verum