consider N being Element of NAT such that
A1: for n being Element of NAT st n >= N holds
g . n > 0 by Def6;
take N ; :: according to ASYMPT_0:def 6 :: thesis: for n being Element of NAT st n >= N holds
(max (f,g)) . n > 0
let n be Element of NAT ; :: thesis: ( n >= N implies (max (f,g)) . n > 0 )
assume n >= N ; :: thesis: (max (f,g)) . n > 0
then g . n > 0 by A1;
then max ((f . n),(g . n)) > 0 by XXREAL_0:25;
hence (max (f,g)) . n > 0 by Def10; :: thesis: verum