let k be Nat; :: thesis: for a being Real
for y being Real_Sequence st 0 <= a & ( for i being Nat holds y . i = a * (i to_power k) ) holds
y in Big_Oh (seq_n^ k)
let a be Real; :: thesis: for y being Real_Sequence st 0 <= a & ( for i being Nat holds y . i = a * (i to_power k) ) holds
y in Big_Oh (seq_n^ k)
let y be Real_Sequence; :: thesis: ( 0 <= a & ( for i being Nat holds y . i = a * (i to_power k) ) implies y in Big_Oh (seq_n^ k) )
assume AS: ( 0 <= a & ( for n being Nat holds y . n = a * (n to_power k) ) ) ; :: thesis: y in Big_Oh (seq_n^ k)
set c = a + 1;
XA1: a + 0 < a + 1 by XREAL_1:8;

A1: now :: thesis: for n being Element of NAT st n >= 2 holds
( y . n <= (a + 1) * ((seq_n^ k) . n) & y . n >= 0 )

let n be Element of NAT ; :: thesis: ( n >= 2 implies ( y . n <= (a + 1) * ((seq_n^ k) . n) & y . n >= 0 ) )
assume A2: n >= 2 ; :: thesis: ( y . n <= (a + 1) * ((seq_n^ k) . n) & y . n >= 0 )
A4: (seq_n^ k) . n = n to_power k by A2, ASYMPT_1:def 3;
then A5: y . n = a * ((seq_n^ k) . n) by AS;
hence y . n <= (a + 1) * ((seq_n^ k) . n) by XA1, A4, XREAL_1:64; :: thesis: y . n >= 0
thus y . n >= 0 by A4, A5, AS; :: thesis: verum

end;

y is Element of Funcs (NAT,REAL) by FUNCT_2:8;
hence y in Big_Oh (seq_n^ k) by AS, A1; :: thesis: verum