set X = the Real-Valued-Random-Variable of Sigma;

now :: thesis: for x being object st x in dom (abs the Real-Valued-Random-Variable of Sigma) holds
0 <= (abs the Real-Valued-Random-Variable of Sigma) . x

let x be object ; :: thesis: ( x in dom (abs the Real-Valued-Random-Variable of Sigma) implies 0 <= (abs the Real-Valued-Random-Variable of Sigma) . x )
assume x in dom (abs the Real-Valued-Random-Variable of Sigma) ; :: thesis: 0 <= (abs the Real-Valued-Random-Variable of Sigma) . x
then (abs the Real-Valued-Random-Variable of Sigma) . x = |.( the Real-Valued-Random-Variable of Sigma . x).| by VALUED_1:def 11;
hence 0 <= (abs the Real-Valued-Random-Variable of Sigma) . x by COMPLEX1:46; :: thesis: verum

end;

then abs the Real-Valued-Random-Variable of Sigma is nonnegative by MESFUNC6:52;
hence ex b₁ being Real-Valued-Random-Variable of Sigma st b₁ is nonnegative ; :: thesis: verum