:: deftheorem Def4 defines seq_n! ASYMPT_1:def 5 :
for a being Element of NAT
for b₂ being Real_Sequence holds
( b₂ = seq_n! a iff for n being Element of NAT holds b₂ . n = (n + a) ! );