theorem :: ASYMPT_2:23

for a being Real st 1 <= a holds
seq_a^ (a,1,0) is non-decreasing