theorem :: ASYMPT_1:8

for f being Real_Sequence st ( for n being Element of NAT st n > 0 holds
f . n = n to_power (log (2,n)) ) holds
ex s being eventually-positive Real_Sequence st
( s = f & not s is smooth )