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:121;
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 7;
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 7;
reconsider k = [/c\] as Element of NAT by A10, INT_1:3;
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:8;
f = seq_n^ 1 by A3, TARSKI:def 1;
then f . n = n to_power 1 by A15, A14, Def3
.= n by POWER:25 ;
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 n to_power (g . n) >= n to_power 0 by A6, A16, PRE_FF:8, A9;
hence 1 <= h . n by A18, POWER:24; :: thesis:
A20: (seq_const 1) . n = 1 by FUNCOP_1:7;
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:8;
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:8;
reconsider t = h as Element of Funcs (NAT,REAL) by FUNCT_2:8;
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:
reconsider N = max (N0,2) as Element of REAL by XREAL_0:def 1;
defpred S₁[ Element of NAT , Real] means ( ( $1 < N implies $2 = 1 ) & ( $1 >= N implies $2 = log ($1,(t . $1)) ) );
A22: N >= 2 by XXREAL_0:25;
then A23: N > 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 A25: n < N ; :: thesis:

1 in REAL by XREAL_0:def 1;
hence ex y being Element of REAL st S₁[n,y] by A25; :: thesis:

end;

suppose A26: n >= N ; :: thesis:

reconsider y = log (n,(t . n)) as Element of REAL by XREAL_0:def 1;
take y ; :: thesis:
thus S₁[n,y] by A26; :: thesis:

end;

consider g being sequence of REAL such that
A27: for x being Element of NAT holds S₁[x,g . x] from FUNCT_2:sch 3(A24);
A28: N >= N0 by XXREAL_0:25;

A29: now :: thesis:

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

end;

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

now :: thesis:

log (N,1) = 0 by A37, A32, POWER:51;
then log (N,(max (c,2))) > 0 by A23, A34, POWER:57;
hence k + (log (N,(max (c,2)))) > 0 ; :: thesis:
let n be Element of NAT ; :: thesis:
A38: (seq_const 1) . n = 1 by FUNCOP_1:7;
assume A39: n >= N ; :: thesis:
then A40: n <> 1 by A22, XXREAL_0:2;
A41: (seq_n^ k) . n = n to_power k by A22, A39, Def3;
then A42: c * ((seq_n^ k) . n) <= (max (c,2)) * ((seq_n^ k) . n) by XREAL_1:64, XXREAL_0:25;
(seq_n^ k) . n > 0 by A22, A39, A41, POWER:34;
then A43: log (n,((max (c,2)) * ((seq_n^ k) . n))) = (log (n,(max (c,2)))) + (log (n,(n to_power k))) by A22, A33, A39, A40, A41, POWER:53
.= (log (n,(max (c,2)))) + (k * (log (n,n))) by A22, A39, A40, POWER:55
.= (log (n,(max (c,2)))) + (k * 1) by A22, A39, A40, POWER:52 ;
log (N,(max (c,2))) >= log (n,(max (c,2))) by A23, A34, A39, Lm19;
then A44: (log (n,(max (c,2)))) + k <= (log (N,(max (c,2)))) + k by XREAL_1:6;
A45: n >= N0 by A28, A39, XXREAL_0:2;
then A46: 1 <= t . n by A21;
t . n = (f . n) to_power (g . n) by A29, A39
.= (n to_power 1) to_power (g . n) by A22, A39, Def3
.= n to_power (g . n) by POWER:25 ;
then A47: log (n,(t . n)) = (g . n) * (log (n,n)) by A22, A39, A40, POWER:55
.= (g . n) * 1 by A22, A39, A40, POWER:52 ;
n >= 2 by A22, A39, XXREAL_0:2;
then A48: n > 1 by XXREAL_0:2;
t . n <= c * ((seq_n^ k) . n) by A21, A45;
then t . n <= (max (c,2)) * ((seq_n^ k) . n) by A42, XXREAL_0:2;
then log (n,(t . n)) <= log (n,((max (c,2)) * ((seq_n^ k) . n))) by A48, A46, PRE_FF:10;
hence g . n <= (k + (log (N,(max (c,2))))) * ((seq_const 1) . n) by A47, A43, A44, A38, XXREAL_0:2; :: thesis:
g . n = log (n,(t . n)) by A27, A39;
then g . n >= log (n,1) by A48, A46, PRE_FF:10;
hence g . n >= 0 by A22, A39, A40, POWER:51; :: thesis:

end;

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