:: deftheorem Def2 defines seq_logn ASYMPT_1:def 2 :
for b₁ being Real_Sequence holds
( b₁ = seq_logn iff ( b₁ . 0 = 0 & ( for n being Element of NAT st n > 0 holds
b₁ . n = log (2,n) ) ) );