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

hereby :: thesis:

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

end;

reconsider f = seq_n^ 1 as Element of Funcs NAT ,REAL by FUNCT_2:11;
reconsider t = h as Element of Funcs NAT ,REAL by FUNCT_2:11;
given N0 being Element of NAT , c being Real, k being Element of NAT such that c > 0 and
A21: for n being Element of NAT st n >= N0 holds
( 1 <= h . n & h . n <= c * ((seq_n^ k) . n) ) ; :: thesis:
set N = max N0,2;
defpred S₁[ Element of NAT , Real] means ( ( $1 < max N0,2 implies $2 = 1 ) & ( $1 >= max N0,2 implies $2 = log $1,(t . $1) ) );
A22: max N0,2 >= 2 by XXREAL_0:25;
then A23: max N0,2 > 1 by XXREAL_0:2;
A24: 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
A25: for x being Element of NAT holds S₁[x,g . x] from FUNCT_2:sch 3(A24);
A26: max N0,2 >= N0 by XXREAL_0:25;

A27: now

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

end;

set c1 = max c,2;
A30: max N0,2 <> 1 by XXREAL_0:25;
set a = log (max N0,2),(max c,2);
set b = k + (log (max N0,2),(max c,2));
A31: max c,2 >= 2 by XXREAL_0:25;
then A32: max c,2 > 1 by XXREAL_0:2;
A33: f in F by TARSKI:def 1;
A34: g is Element of Funcs NAT ,REAL by FUNCT_2:11;
A35: max N0,2 > 0 by XXREAL_0:25;

now

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

end;

then g in Big_Oh (seq_const 1) by A34;
hence h in F to_power (Big_Oh (seq_const 1)) by A34, A27, A33; :: 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: