:: deftheorem defines + ASYMPT_0:def 18 :
for X being non empty set
for F, G being FUNCTION_DOMAIN of X, REAL holds F + G = { t where t is Element of Funcs (X,REAL) : ex f, g being Element of Funcs (X,REAL) st
( f in F & g in G & ( for n being Element of X holds t . n = (f . n) + (g . n) ) ) } ;