for g being Real_Sequence st ( for n being Element of NAT holds g . n = (((n ^2) - n) + 1) to_power 4 ) holds
ex s being eventually-positive Real_Sequence st
( s = g & Big_Oh (seq_n^ 8) = Big_Oh s )