for x being ExtReal holds x / +infty = 0 ;