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, Def3;
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;
then A7: f | E = f by A4, FUNCT_2:40;
f + g is_integrable_on P2M P by A3, MESFUNC6:100;
then f + g is_integrable_on P by Def3;
hence expect (f + g),P = Integral (P2M P),(f + g) by Def4
.= (Integral (P2M P),f) + (Integral (P2M P),g) by A4, A5, A6, A7, FUNCT_2:40
.= (expect f,P) + (expect g,P) by A2, SUPINF_2:1 ;
:: thesis: verum