consider X being Real-Valued-Random-Variable of Sigma;

now

let x be set ; :: thesis: ( x in dom (abs X) implies 0 <= (abs X) . x )
assume x in dom (abs X) ; :: thesis: 0 <= (abs X) . x
then (abs X) . x = abs (X . x) by VALUED_1:def 11;
hence 0 <= (abs X) . x by COMPLEX1:132; :: thesis: verum

end;

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