let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega
for f being Real-Valued-Random-Variable of Sigma holds abs f is Real-Valued-Random-Variable of Sigma
let Sigma be SigmaField of Omega; :: thesis: for f being Real-Valued-Random-Variable of Sigma holds abs f is Real-Valued-Random-Variable of Sigma
let f be Real-Valued-Random-Variable of Sigma; :: thesis: abs f is Real-Valued-Random-Variable of Sigma
consider X being Element of Sigma such that
A1: X = Omega and
A2: f is_measurable_on X by Def2;
( dom f = X & R_EAL f is_measurable_on X ) by A1, A2, FUNCT_2:def 1, MESFUNC6:def 6;
then |.(R_EAL f).| is_measurable_on X by MESFUNC2:29;
then R_EAL (abs f) is_measurable_on X by MESFUNC6:1;
then abs f is_measurable_on X by MESFUNC6:def 6;
hence abs f is Real-Valued-Random-Variable of Sigma by A1, Def2; :: thesis: verum