:: deftheorem Def3 defines seq_n^ ASYMPT_1:def 3 :
for a being Real
for b₂ being Real_Sequence holds
( b₂ = seq_n^ a iff ( b₂ . 0 = 0 & ( for n being Element of NAT st n > 0 holds
b₂ . n = n to_power a ) ) );