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 SUPINF_2:51;
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 nonpositive by MESFUNC5:8; :: thesis: verum