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: ex X being Element of Sigma st
( X = Omega & f is_measurable_on X ) by Def2;
consider Y being Element of Sigma such that
A2: Y = Omega and
A3: g is_measurable_on Y by Def2;
dom g = Y by A2, FUNCT_2:def 1;
hence f - g is Real-Valued-Random-Variable of Sigma by A1, A2, A3, Def2, MESFUNC6:29; :: thesis: verum