for k being Nat
for a being Real
for y being Real_Sequence st 0 <= a & ( for i being Nat holds y . i = a * (i to_power k) ) holds
y in Big_Oh (seq_n^ k)