:: deftheorem Def1 defines seq_a^ ASYMPT_1:def 1 :
for a, b, c being Real
for b₄ being Real_Sequence holds
( b₄ = seq_a^ (a,b,c) iff for n being Element of NAT holds b₄ . n = a to_power ((b * n) + c) );