let f be eventually-nonnegative Real_Sequence; :: thesis: for k being Nat st f in Big_Oh () holds
ex N being Nat st
for n being Nat st N <= n holds
f . n <= (seq_n^ (k + 1)) . n

let k be Nat; :: thesis: ( f in Big_Oh () implies ex N being Nat st
for n being Nat st N <= n holds
f . n <= (seq_n^ (k + 1)) . n )

assume f in Big_Oh () ; :: thesis: ex N being Nat st
for n being Nat st N <= n holds
f . n <= (seq_n^ (k + 1)) . n

then consider t being Element of Funcs (NAT,REAL) such that
L1: ( f = t & ex c being Real ex N being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( t . n <= c * (() . n) & t . n >= 0 ) ) ) ) ;
consider c being Real, N being Element of NAT such that
L2: ( c > 0 & ( for n being Element of NAT st n >= N holds
( f . n <= c * (() . n) & f . n >= 0 ) ) ) by L1;
set n = [/(max (N,c))\];
P1: ( N <= max (N,c) & c <= max (N,c) ) by XXREAL_0:25;
P2P: max (N,c) <= [/(max (N,c))\] by INT_1:def 7;
then P2: ( N <= [/(max (N,c))\] & c <= [/(max (N,c))\] ) by ;
reconsider n = [/(max (N,c))\] as Element of NAT by ;
take n ; :: thesis: for n being Nat st n <= n holds
f . n <= (seq_n^ (k + 1)) . n

let x be Nat; :: thesis: ( n <= x implies f . x <= (seq_n^ (k + 1)) . x )
A: x in NAT by ORDINAL1:def 12;
assume P4: n <= x ; :: thesis: f . x <= (seq_n^ (k + 1)) . x
then P4r: ( 0 < x & N <= x & c <= x ) by ;
P5: (seq_n^ (k + 1)) . x = x * (() . x) by ;
P6: ( f . x <= c * (() . x) & f . x >= 0 ) by A, P4r, L2;
(seq_n^ k) . x = x to_power k by ;
then c * (() . x) <= x * (() . x) by ;
hence f . x <= (seq_n^ (k + 1)) . x by ; :: thesis: verum