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

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

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

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

then reconsider x1 = x as Element of X ;
(- f) . x = - (f . x1) by A1, MESFUNC1:def 7;
hence (- f) . x > -infty by XXREAL_3:6, XXREAL_3:38, MESFUNC5:def 6; :: thesis: verum

end;

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

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

end;

end;

end;

hence - f is without-infty by MESFUNC5:def 5; :: thesis: verum