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