consider N being Nat such that
A1: for n being Nat st n >= N holds
g . n >= 0 by Def2;
take N ; :: according to ASYMPT_0:def 2 :: thesis: for n being Nat st n >= N holds
(max (f,g)) . n >= 0
let n be Nat; :: thesis: ( n >= N implies (max (f,g)) . n >= 0 )
assume n >= N ; :: thesis: (max (f,g)) . n >= 0
then A2: g . n >= 0 by A1;
max ((f . n),(g . n)) >= g . n by XXREAL_0:25;
hence (max (f,g)) . n >= 0 by A2, Def7; :: thesis: verum