for e being positive Real
for f being Real_Sequence st f . 0 = 0 & ( for n being Element of NAT st n > 0 holds
f . n = log (2,(n to_power e)) ) holds
( f /" (seq_n^ e) is convergent & lim (f /" (seq_n^ e)) = 0 ) by Lm10;