for f being Real_Sequence st ( for n being Element of NAT st n > 0 holds
f . n = n to_power (sqrt n) ) holds
ex s, s1 being eventually-positive Real_Sequence st
( s = f & s1 = seq_a^ (2,1,0) & Big_Oh s c= Big_Oh s1 & not Big_Oh s = Big_Oh s1 )