theorem Th9: :: ASYMPT_1:9

for f being eventually-nonnegative Real_Sequence ex F being FUNCTION_DOMAIN of NAT , REAL st
( F = {(seq_n^ 1)} & ( f in F to_power (Big_Oh (seq_const 1)) implies ex N being Element of NAT ex c being Real ex k being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( 1 <= f . n & f . n <= c * ((seq_n^ k) . n) ) ) ) ) & ( ex N being Element of NAT ex c being Real ex k being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( 1 <= f . n & f . n <= c * ((seq_n^ k) . n) ) ) ) implies f in F to_power (Big_Oh (seq_const 1)) ) )