for f being eventually-nonnegative Real_Sequence st ex b being Element of NAT st
( b >= 2 & f is_smooth_wrt b ) holds
f is smooth