set f = seq_n^ 8;
let e be Real; :: thesis: ( 0 < e & e < 1 implies ex s being eventually-positive Real_Sequence st
( s = seq_a^ (1 + e),1,0 & Big_Oh (seq_n^ 8) c= Big_Oh s & not Big_Oh (seq_n^ 8) = Big_Oh s ) )
assume that
A1: 0 < e and
A2: e < 1 ; :: thesis: ex s being eventually-positive Real_Sequence st
( s = seq_a^ (1 + e),1,0 & Big_Oh (seq_n^ 8) c= Big_Oh s & not Big_Oh (seq_n^ 8) = Big_Oh s )
consider N being Element of NAT such that
A3: for n being Element of NAT st n >= N holds
(n * (log 2,(1 + e))) - (8 * (log 2,n)) > 8 * (log 2,n) by A1, A2, Lm25;
set g = seq_a^ (1 + e),1,0 ;
set h = (seq_n^ 8) /" (seq_a^ (1 + e),1,0 );
reconsider g = seq_a^ (1 + e),1,0 as eventually-positive Real_Sequence by A1;
take g ; :: thesis: ( g = seq_a^ (1 + e),1,0 & Big_Oh (seq_n^ 8) c= Big_Oh g & not Big_Oh (seq_n^ 8) = Big_Oh g )
thus g = seq_a^ (1 + e),1,0 ; :: thesis: ( Big_Oh (seq_n^ 8) c= Big_Oh g & not Big_Oh (seq_n^ 8) = Big_Oh g )

A4: now

let p be real number ; :: thesis: ( p > 0 implies ex N1 being Element of NAT st
for n being Element of NAT st n >= N1 holds
abs ((((seq_n^ 8) /" (seq_a^ (1 + e),1,0 )) . n) - 0 ) < p )
assume A5: p > 0 ; :: thesis: ex N1 being Element of NAT st
for n being Element of NAT st n >= N1 holds
abs ((((seq_n^ 8) /" (seq_a^ (1 + e),1,0 )) . n) - 0 ) < p
reconsider p1 = p as Real by XREAL_0:def 1;
A6: (1 / p1) to_power (1 / 8) > 0 by A5, POWER:39;
set N1 = max N,(max [/((1 / p1) to_power (1 / 8))\],2);
A7: max N,(max [/((1 / p1) to_power (1 / 8))\],2) >= N by XXREAL_0:25;
A8: max N,(max [/((1 / p1) to_power (1 / 8))\],2) is Integer

proof

per cases ( max N,(max [/((1 / p1) to_power (1 / 8))\],2) = N or max N,(max [/((1 / p1) to_power (1 / 8))\],2) = max [/((1 / p) to_power (1 / 8))\],2 ) by XXREAL_0:16;

suppose max N,(max [/((1 / p1) to_power (1 / 8))\],2) = N ; :: thesis: max N,(max [/((1 / p1) to_power (1 / 8))\],2) is Integer

hence max N,(max [/((1 / p1) to_power (1 / 8))\],2) is Integer ; :: thesis: verum

end;

suppose max N,(max [/((1 / p1) to_power (1 / 8))\],2) = max [/((1 / p) to_power (1 / 8))\],2 ; :: thesis: max N,(max [/((1 / p1) to_power (1 / 8))\],2) is Integer

hence max N,(max [/((1 / p1) to_power (1 / 8))\],2) is Integer by XXREAL_0:16; :: thesis: verum

end;

end;

end;

A9: max N,(max [/((1 / p1) to_power (1 / 8))\],2) >= max [/((1 / p) to_power (1 / 8))\],2 by XXREAL_0:25;
max [/((1 / p) to_power (1 / 8))\],2 >= [/((1 / p) to_power (1 / 8))\] by XXREAL_0:25;
then A10: max N,(max [/((1 / p1) to_power (1 / 8))\],2) >= [/((1 / p) to_power (1 / 8))\] by A9, XXREAL_0:2;
reconsider N1 = max N,(max [/((1 / p1) to_power (1 / 8))\],2) as Element of NAT by A7, A8, INT_1:16;
take N1 = N1; :: thesis: for n being Element of NAT st n >= N1 holds
abs ((((seq_n^ 8) /" (seq_a^ (1 + e),1,0 )) . n) - 0 ) < p
let n be Element of NAT ; :: thesis: ( n >= N1 implies abs ((((seq_n^ 8) /" (seq_a^ (1 + e),1,0 )) . n) - 0 ) < p )
assume A11: n >= N1 ; :: thesis: abs ((((seq_n^ 8) /" (seq_a^ (1 + e),1,0 )) . n) - 0 ) < p
then n >= N by A7, XXREAL_0:2;
then (n * (log 2,(1 + e))) - (8 * (log 2,n)) > 8 * (log 2,n) by A3;
then A12: 2 to_power ((n * (log 2,(1 + e))) - (8 * (log 2,n))) > 2 to_power (8 * (log 2,n)) by POWER:44;
A13: max [/((1 / p) to_power (1 / 8))\],2 >= 2 by XXREAL_0:25;
A14: g . n = (1 + e) to_power ((1 * n) + 0 ) by Def1;
((seq_n^ 8) /" (seq_a^ (1 + e),1,0 )) . n = ((seq_n^ 8) . n) / (g . n) by Lm4;
then A15: ((seq_n^ 8) /" (seq_a^ (1 + e),1,0 )) . n = (n to_power 8) / ((1 + e) to_power n) by A9, A13, A11, A14, Def3
.= (2 to_power (8 * (log 2,n))) / ((1 + e) to_power n) by A9, A13, A11, Lm3
.= (2 to_power (8 * (log 2,n))) / (2 to_power (n * (log 2,(1 + e)))) by A1, Lm3
.= 2 to_power ((8 * (log 2,n)) - (n * (log 2,(1 + e)))) by POWER:34
.= 2 to_power (- ((n * (log 2,(1 + e))) - (8 * (log 2,n)))) ;
[/((1 / p) to_power (1 / 8))\] >= (1 / p) to_power (1 / 8) by INT_1:def 5;
then N1 >= (1 / p) to_power (1 / 8) by A10, XXREAL_0:2;
then n >= (1 / p) to_power (1 / 8) by A11, XXREAL_0:2;
then n to_power 8 >= ((1 / p) to_power (1 / 8)) to_power 8 by A6, Lm6;
then n to_power 8 >= (1 / p1) to_power ((1 / 8) * 8) by A5, POWER:38;
then n to_power 8 >= 1 / p1 by POWER:30;
then 1 / (n to_power 8) <= 1 / (p " ) by A5, XREAL_1:87;
then 1 / (2 to_power (8 * (log 2,n))) <= p by A9, A13, A11, Lm3;
then A16: 2 to_power (- (8 * (log 2,n))) <= p by POWER:33;
2 to_power (8 * (log 2,n)) > 0 by POWER:39;
then 1 / (2 to_power ((n * (log 2,(1 + e))) - (8 * (log 2,n)))) < 1 / (2 to_power (8 * (log 2,n))) by A12, XREAL_1:90;
then 2 to_power (- ((n * (log 2,(1 + e))) - (8 * (log 2,n)))) < 1 / (2 to_power (8 * (log 2,n))) by POWER:33;
then ((seq_n^ 8) /" (seq_a^ (1 + e),1,0 )) . n < 2 to_power (- (8 * (log 2,n))) by A15, POWER:33;
then A17: ((seq_n^ 8) /" (seq_a^ (1 + e),1,0 )) . n < p by A16, XXREAL_0:2;
((seq_n^ 8) /" (seq_a^ (1 + e),1,0 )) . n > 0 by A15, POWER:39;
hence abs ((((seq_n^ 8) /" (seq_a^ (1 + e),1,0 )) . n) - 0 ) < p by A17, ABSVALUE:def 1; :: thesis: verum

end;

then A18: (seq_n^ 8) /" (seq_a^ (1 + e),1,0 ) is convergent by SEQ_2:def 6;
then A19: lim ((seq_n^ 8) /" (seq_a^ (1 + e),1,0 )) = 0 by A4, SEQ_2:def 7;
then not g in Big_Oh (seq_n^ 8) by A18, ASYMPT_0:16;
then A20: not seq_n^ 8 in Big_Omega g by ASYMPT_0:19;
seq_n^ 8 in Big_Oh g by A18, A19, ASYMPT_0:16;
hence ( Big_Oh (seq_n^ 8) c= Big_Oh g & not Big_Oh (seq_n^ 8) = Big_Oh g ) by A20, Th4; :: thesis: verum