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

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

end;

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