for e being Real st 0 < e & e < 1 holds
ex s being eventually-positive Real_Sequence st
( s = seq_a^ ((1 + e),1,0) & Big_Oh (seq_n^ 8) c= Big_Oh s & not Big_Oh (seq_n^ 8) = Big_Oh s )