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 ()

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 ()

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 () )
assume AS: ( 0 <= a & ( for n being Nat holds y . n = a * (n to_power k) ) ) ; :: thesis: y in Big_Oh ()
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) * (() . n) & y . n >= 0 )
let n be Element of NAT ; :: thesis: ( n >= 2 implies ( y . n <= (a + 1) * (() . n) & y . n >= 0 ) )
assume A2: n >= 2 ; :: thesis: ( y . n <= (a + 1) * (() . n) & y . n >= 0 )
A4: (seq_n^ k) . n = n to_power k by ;
then A5: y . n = a * (() . n) by AS;
hence y . n <= (a + 1) * (() . n) by ; :: 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 () by AS, A1; :: thesis: verum