:: deftheorem Def7 defines max ASYMPT_0:def 7 :
for f, g, b₃ being Real_Sequence holds
( b₃ = max (f,g) iff for n being Nat holds b₃ . n = max ((f . n),(g . n)) );