:: deftheorem Def15 defines taken_every ASYMPT_0:def 15 :

for f being Real_Sequence

for b being Nat

for b_{3} being Real_Sequence holds

( b_{3} = f taken_every b iff for n being Element of NAT holds b_{3} . n = f . (b * n) );

for f being Real_Sequence

for b being Nat

for b

( b