for f being ExtReal holds (- f) " = - (f ")