:: deftheorem defines smooth ASYMPT_0:def 17 :
for f being eventually-nonnegative Real_Sequence holds
( f is smooth iff for b being Element of NAT st b >= 2 holds
f is_smooth_wrt b );