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 AS0: ( f is_integrable_on P & g is_integrable_on P ) ; :: thesis: expect (f - g),P = (expect f,P) - (expect g,P)
then g is_integrable_on P2M P by defintf;
then (- 1) (#) g is_integrable_on P2M P by MESFUNC6:102;
then P1: (- 1) (#) g is_integrable_on P by defintf;
thus expect (f - g),P = (expect f,P) + (expect ((- 1) (#) g),P) by P1, AS0, EXPFG
.= (expect f,P) + ((- 1) * (expect g,P)) by AS0, EXPRF
.= (expect f,P) - (expect g,P) ; :: thesis: verum