theorem :: ASYMPT_1:62

for a being logbase Real
for f being Real_Sequence st a > 1 & f . 0 = 0 & ( for n being Element of NAT st n > 0 holds
f . n = log (a,n) ) holds
f is eventually-positive by Lm2;