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
A2: f is [#] Sigma -measurable ;
( dom f = [#] Sigma & R_EAL f is [#] Sigma -measurable ) by A2, FUNCT_2:def 1;
then |.(R_EAL f).| is [#] Sigma -measurable by MESFUNC2:27;
then R_EAL (abs f) is [#] Sigma -measurable by MESFUNC6:1;
then abs f is [#] Sigma -measurable ;
hence abs f is Real-Valued-Random-Variable of Sigma ; :: thesis: verum