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, Def3;
then (- 1) (#) g is_integrable_on P2M P by MESFUNC6:102;
then (- 1) (#) g is_integrable_on P by Def3;
hence expect (f - g),P = (expect f,P) + (expect ((- 1) (#) g),P) by A1, Th26
.= (expect f,P) + ((- 1) * (expect g,P)) by A2, Th27
.= (expect f,P) - (expect g,P) ;
:: thesis: verum