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)) )
set h = f + g;
assume A1: ( f is_integrable_on P & g is_integrable_on P ) ; :: thesis: expect ((f + g),P) = (expect (f,P)) + (expect (g,P))
then A2: ( Integral ((P2M P),f) = expect (f,P) & Integral ((P2M P),g) = expect (g,P) ) by Def4;
A3: ( f is_integrable_on P2M P & g is_integrable_on P2M P ) by A1;
then consider E being Element of Sigma such that
A4: E = (dom f) /\ (dom g) and
A5: Integral ((P2M P),(f + g)) = (Integral ((P2M P),(f | E))) + (Integral ((P2M P),(g | E))) by MESFUNC6:101;
A6: ( dom f = Omega & dom g = Omega ) by FUNCT_2:def 1;
f + g is_integrable_on P2M P by A3, MESFUNC6:100;
then f + g is_integrable_on P ;
hence expect ((f + g),P) = Integral ((P2M P),(f + g)) by Def4
.= (Integral ((P2M P),f)) + (Integral ((P2M P),g)) by A4, A5, A6
.= (expect (f,P)) + (expect (g,P)) by A2, SUPINF_2:1 ;
:: thesis: verum