now :: thesis: for x being object st x in dom (abs X) holds
0 <= (abs X) . x

let x be object ; :: 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 = |.(X . x).| by VALUED_1:def 11;
hence 0 <= (abs X) . x by COMPLEX1:46; :: thesis: verum

end;

hence abs X is nonnegative by MESFUNC6:52; :: thesis: verum