theorem :: ASYMPT_2:23
for a being Real st 1 <= a holds
seq_a^ (a,1,0) is V51()