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
A1: f is [#] Sigma -measurable by Def2;
set Y = [#] Sigma;
A3: g is [#] Sigma -measurable by Def2;
dom g = [#] Sigma by FUNCT_2:def 1;
then f - g is [#] Sigma -measurable by MESFUNC6:29, A1, A3;
hence f - g is Real-Valued-Random-Variable of Sigma by Def2; :: thesis: verum