now :: thesis: for x being object holds (- f) . x >= 0

let x be object ; :: thesis: (- f) . b₁ >= 0

per cases ( x in dom (- f) or not x in dom (- f) ) ;

suppose A1: x in dom (- f) ; :: thesis: (- f) . b₁ >= 0

then reconsider x1 = x as Element of X ;
A2: (- f) . x = - (f . x1) by A1, MESFUNC1:def 7;
f . x1 <= 0 by MESFUNC5:8;
hence (- f) . x >= 0 by A2; :: thesis: verum

end;

suppose not x in dom (- f) ; :: thesis: (- f) . b₁ >= 0

hence (- f) . x >= 0 by FUNCT_1:def 2; :: thesis: verum

end;

end;

end;

hence - f is nonnegative by SUPINF_2:51; :: thesis: verum