for x being object st x in dom (- f) holds
0 <= (- f) . x
proof
let x be object ; :: thesis: ( x in dom (- f) implies 0 <= (- f) . x )
assume A1: x in dom (- f) ; :: thesis: 0 <= (- f) . x
f . x <= 0 by MESFUNC5:8;
then - (f . x) >= 0 ;
hence (- f) . x >= 0 by A1, MESFUNC1:def 7; :: thesis: verum
end;
hence - f is nonnegative by SUPINF_2:52; :: thesis: verum