:: deftheorem defines max ASYMPT_0:def 19 :
for X being non empty set
for F, G being FUNCTION_DOMAIN of X, REAL holds max (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 = max ((f . n),(g . n)) ) ) } ;