theorem :: MESFUN11:24

for X being non empty set
for f1, f2 being Function of X,ExtREAL st f2 is without-infty & f2 is without+infty holds
( f1 + f2 is Function of X,ExtREAL & ( for x being Element of X holds (f1 + f2) . x = (f1 . x) + (f2 . x) ) )