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 AS: ( f is_integrable_on P2M P & g is_integrable_on P2M P ) by defintf;
set h = f + g;
consider E being Element of Sigma such that
P1: ( E = (dom f) /\ (dom g) & Integral (P2M P),(f + g) = (Integral (P2M P),(f | E)) + (Integral (P2M P),(g | E)) ) by AS, MESFUNC6:101;
P2: ( dom f = Omega & dom g = Omega ) by FUNCT_2:def 1;
P5: f | E = f by P2, P1, FUNCT_2:40;
P7: Integral (P2M P),f = expect f,P by def2, AS0;
P8: Integral (P2M P),g = expect g,P by def2, AS0;
f + g is_integrable_on P2M P by AS, MESFUNC6:100;
then f + g is_integrable_on P by defintf;
hence expect (f + g),P = Integral (P2M P),(f + g) by def2
.= (Integral (P2M P),f) + (Integral (P2M P),g) by P2, P1, FUNCT_2:40, P5
.= (expect f,P) + (expect g,P) by P7, P8, SUPINF_2:1 ;
:: thesis: verum