now :: thesis: for x being set st x in dom (- f) holds
(- f) . x < +infty

let x be set ; :: thesis: ( x in dom (- f) implies (- f) . x < +infty )
assume A1: x in dom (- f) ; :: thesis: (- f) . x < +infty
then x in dom f by MESFUNC1:def 7;
then (f . x) * (- 1) < -infty * (- 1) by MESFUNC5:10, XXREAL_3:102;
then (f . x) * (- 1) < - -infty by XXREAL_3:91;
then - (f . x) < +infty by XXREAL_3:5, XXREAL_3:91;
hence (- f) . x < +infty by A1, MESFUNC1:def 7; :: thesis: verum

end;

hence - f is without+infty by MESFUNC5:11; :: thesis: verum