for e being Real st e > 0 holds
( seq_logn /" (seq_n^ e) is convergent & lim (seq_logn /" (seq_n^ e)) = 0 ) by Lm11;