theorem Th9: :: MESFUN12:9

for X being non empty set
for f being Function of X,ExtREAL holds f + (X --> 0.) = f