let h be eventually-nonnegative Real_Sequence; :: thesis:
reconsider F = {(seq_n^ 1)} as FUNCTION_DOMAIN of NAT , REAL by FRAENKEL:10;
take F ; :: thesis:
thus F = {(seq_n^ 1)} ; :: thesis:
set G = Big_Oh (seq_const 1);
set p = seq_const 1;

now

hereby :: thesis:

assume h in F to_power (Big_Oh (seq_const 1)) ; :: thesis:
then consider t being Element of Funcs NAT ,REAL such that
A1: h = t and
A2: ex f, g being Element of Funcs NAT ,REAL ex N being Element of NAT st
( f in F & g in Big_Oh (seq_const 1) & ( for n being Element of NAT st n >= N holds
t . n = (f . n) to_power (g . n) ) ) ;
consider f, g being Element of Funcs NAT ,REAL , N0 being Element of NAT such that
A3: f in F and
A4: g in Big_Oh (seq_const 1) and
A5: for n being Element of NAT st n >= N0 holds
t . n = (f . n) to_power (g . n) by A2;
A6: f = seq_n^ 1 by A3, TARSKI:def 1;
consider g' being Element of Funcs NAT ,REAL such that
A7: g = g' and
A8: ex c being Real ex N being Element of NAT st
( c > 0 & ( for n being Element of NAT st n >= N holds
( g' . n <= c * ((seq_const 1) . n) & g' . n >= 0 ) ) ) by A4;
consider c being Real, N1 being Element of NAT such that
A9: c > 0 and
A10: for n being Element of NAT st n >= N1 holds
( g' . n <= c * ((seq_const 1) . n) & g' . n >= 0 ) by A8;
set N = max 2,(max N0,N1);
( max N0,N1 >= N0 & max N0,N1 >= N1 & max 2,(max N0,N1) >= max N0,N1 ) by XXREAL_0:25;
then A11: ( max 2,(max N0,N1) >= N0 & max 2,(max N0,N1) >= N1 & max 2,(max N0,N1) >= 2 ) by XXREAL_0:2, XXREAL_0:25;
set k = [/c\];
A12: [/c\] >= c by INT_1:def 5;
[/c\] > 0 by A9, INT_1:def 5;
then reconsider k = [/c\] as Element of NAT by INT_1:16;
reconsider i = 1 as Element of NAT ;
take N = max 2,(max N0,N1); :: thesis:
take i = i; :: thesis:
take k = k; :: thesis:
thus i > 0 ; :: thesis:
let n be Element of NAT ; :: thesis:
assume A13: n >= N ; :: thesis:
then A14: ( n >= N0 & n >= N1 & n >= 2 ) by A11, XXREAL_0:2;
then A15: ( g' . n <= c * ((seq_const 1) . n) & g' . n >= 0 ) by A10;
A16: (seq_const 1) . n = 1 by FUNCOP_1:13;
A17: ( n > 0 & n > 1 ) by A14, XXREAL_0:2;
f . n = n to_power 1 by A6, A11, A13, Def3
.= n by POWER:30 ;
then A18: h . n = n to_power (g . n) by A1, A5, A11, A13, XXREAL_0:2;
n to_power (g . n) >= n to_power 0 by A7, A15, A17, PRE_FF:10;
hence 1 <= h . n by A18, POWER:29; :: thesis:
g . n <= c * ((seq_const 1) . n) by A7, A10, A14;
then A19: h . n <= n to_power (c * 1) by A16, A17, A18, PRE_FF:10;
n to_power c <= n to_power k by A12, A17, PRE_FF:10;
then h . n <= n to_power k by A19, XXREAL_0:2;
hence h . n <= i * ((seq_n^ k) . n) by A11, A13, Def3; :: thesis:

end;

given N0 being Element of NAT , c being Real, k being Element of NAT such that c > 0 and
A20: for n being Element of NAT st n >= N0 holds
( 1 <= h . n & h . n <= c * ((seq_n^ k) . n) ) ; :: thesis:
reconsider t = h as Element of Funcs NAT ,REAL by FUNCT_2:11;
set N = max N0,2;
A21: ( max N0,2 >= N0 & max N0,2 >= 2 ) by XXREAL_0:25;
then A22: max N0,2 > 1 by XXREAL_0:2;
A23: ( max N0,2 > 0 & max N0,2 <> 1 ) by XXREAL_0:25;
set c1 = max c,2;
A24: ( max c,2 >= c & max c,2 >= 2 ) by XXREAL_0:25;
then A25: ( max c,2 > 0 & max c,2 > 1 ) by XXREAL_0:2;
set a = log (max N0,2),(max c,2);
set b = k + (log (max N0,2),(max c,2));
reconsider f = seq_n^ 1 as Element of Funcs NAT ,REAL by FUNCT_2:11;
defpred S₁[ Element of NAT , Real] means ( ( $1 < max N0,2 implies $2 = 1 ) & ( $1 >= max N0,2 implies $2 = log $1,(t . $1) ) );
A26: for x being Element of NAT ex y being Element of REAL st S₁[x,y]

proof

let n be Element of NAT ; :: thesis:

per cases ;

suppose n < max N0,2 ; :: thesis:

hence ex y being Element of REAL st S₁[n,y] ; :: thesis:

end;

suppose n >= max N0,2 ; :: thesis:

hence ex y being Element of REAL st S₁[n,y] ; :: thesis:

end;

consider g being Function of NAT , REAL such that
A27: for x being Element of NAT holds S₁[x,g . x] from FUNCT_2:sch 3(A26);
A28: g is Element of Funcs NAT ,REAL by FUNCT_2:11;

A29: now

let n be Element of NAT ; :: thesis:
assume A30: n >= max N0,2 ; :: thesis:
then n >= N0 by A21, XXREAL_0:2;
then A31: t . n >= 1 by A20;
thus (f . n) to_power (g . n) = (n to_power 1) to_power (g . n) by A21, A30, Def3
.= n to_power (g . n) by POWER:30
.= n to_power (1 * (log n,(t . n))) by A27, A30
.= t . n by A22, A30, A31, POWER:def 3 ; :: thesis:

end;

A32: f in F by TARSKI:def 1;

now

log (max N0,2),1 = 0 by A23, POWER:59;
then log (max N0,2),(max c,2) > 0 by A22, A25, POWER:65;
then k + (log (max N0,2),(max c,2)) > k + 0 by XREAL_1:8;
hence k + (log (max N0,2),(max c,2)) > 0 ; :: thesis:
let n be Element of NAT ; :: thesis:
assume A33: n >= max N0,2 ; :: thesis:
then A34: ( n >= N0 & n >= 2 ) by A21, XXREAL_0:2;
then A35: n > 1 by XXREAL_0:2;
A36: ( n > 0 & n <> 1 ) by A21, A33, XXREAL_0:2;
A37: log (max N0,2),(max c,2) >= log n,(max c,2) by A22, A25, A33, Lm24;
A38: ( 1 <= t . n & t . n <= c * ((seq_n^ k) . n) ) by A20, A34;
A39: (seq_n^ k) . n = n to_power k by A21, A33, Def3;
then A40: (seq_n^ k) . n > 0 by A21, A33, POWER:39;
c * ((seq_n^ k) . n) <= (max c,2) * ((seq_n^ k) . n) by A39, XREAL_1:66, XXREAL_0:25;
then t . n <= (max c,2) * ((seq_n^ k) . n) by A38, XXREAL_0:2;
then A41: log n,(t . n) <= log n,((max c,2) * ((seq_n^ k) . n)) by A35, A38, PRE_FF:12;
t . n = (f . n) to_power (g . n) by A29, A33
.= (n to_power 1) to_power (g . n) by A21, A33, Def3
.= n to_power (g . n) by POWER:30 ;
then A42: log n,(t . n) = (g . n) * (log n,n) by A36, POWER:63
.= (g . n) * 1 by A36, POWER:60 ;
A43: log n,((max c,2) * ((seq_n^ k) . n)) = (log n,(max c,2)) + (log n,(n to_power k)) by A24, A36, A39, A40, POWER:61
.= (log n,(max c,2)) + (k * (log n,n)) by A36, POWER:63
.= (log n,(max c,2)) + (k * 1) by A36, POWER:60 ;
A44: (log n,(max c,2)) + k <= (log (max N0,2),(max c,2)) + k by A37, XREAL_1:8;
(seq_const 1) . n = 1 by FUNCOP_1:13;
hence g . n <= (k + (log (max N0,2),(max c,2))) * ((seq_const 1) . n) by A41, A42, A43, A44, XXREAL_0:2; :: thesis:
g . n = log n,(t . n) by A27, A33;
then g . n >= log n,1 by A35, A38, PRE_FF:12;
hence g . n >= 0 by A36, POWER:59; :: thesis:

end;

then g in Big_Oh (seq_const 1) by A28;
hence h in F to_power (Big_Oh (seq_const 1)) by A28, A29, A32; :: thesis:

end;

hence ( h in F to_power (Big_Oh (seq_const 1)) iff 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 <= h . n & h . n <= c * ((seq_n^ k) . n) ) ) ) ) ; :: thesis: