:: deftheorem Def15 defines taken_every ASYMPT_0:def 15 :
for f being Real_Sequence
for b being Nat
for b₃ being Real_Sequence holds
( b₃ = f taken_every b iff for n being Element of NAT holds b₃ . n = f . (b * n) );