for f being Real_Sequence st ( for n being Element of NAT holds f . n = Step1 n ) holds
ex s being eventually-positive Real_Sequence st
( s = f & not s is smooth & ( for n being Element of NAT holds f . n <= (seq_n^ 1) . n ) & f is eventually-nondecreasing )