let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for f, g being Real-Valued-Random-Variable of Sigma holds f + g is Real-Valued-Random-Variable of Sigma
let Sigma be SigmaField of Omega; :: thesis: for f, g being Real-Valued-Random-Variable of Sigma holds f + g is Real-Valued-Random-Variable of Sigma
let f, g be Real-Valued-Random-Variable of Sigma; :: thesis: f + g is Real-Valued-Random-Variable of Sigma
( ex X being Element of Sigma st
( X = Omega & f is_measurable_on X ) & ex Y being Element of Sigma st
( Y = Omega & g is_measurable_on Y ) ) by Def2;
hence f + g is Real-Valued-Random-Variable of Sigma by Def2, MESFUNC6:26; :: thesis: verum