for d being XFinSequence of REAL
for k being Nat st len d = 1 & d is nonnegative-yielding holds
seq_p d in Big_Oh (seq_n^ k)