now :: thesis: for x being object st x in dom (abs f) holds

0 <= (abs f) . x

hence
abs f is nonnegative
by MESFUNC6:52; :: thesis: verum0 <= (abs f) . x

let x be object ; :: thesis: ( x in dom (abs f) implies 0 <= (abs f) . x )

assume x in dom (abs f) ; :: thesis: 0 <= (abs f) . x

then (abs f) . x = |.(f . x).| by VALUED_1:def 11;

hence 0 <= (abs f) . x by COMPLEX1:46; :: thesis: verum

end;assume x in dom (abs f) ; :: thesis: 0 <= (abs f) . x

then (abs f) . x = |.(f . x).| by VALUED_1:def 11;

hence 0 <= (abs f) . x by COMPLEX1:46; :: thesis: verum