set g = seq_a^ (2,1,0);
let f be Real_Sequence; :: thesis: ( ( for n being Element of NAT st n > 0 holds
f . n = n to_power (sqrt n) ) implies ex s, s1 being eventually-positive Real_Sequence st
( s = f & s1 = seq_a^ (2,1,0) & Big_Oh s c= Big_Oh s1 & not Big_Oh s = Big_Oh s1 ) )
assume A1: for n being Element of NAT st n > 0 holds
f . n = n to_power (sqrt n) ; :: thesis: ex s, s1 being eventually-positive Real_Sequence st
( s = f & s1 = seq_a^ (2,1,0) & Big_Oh s c= Big_Oh s1 & not Big_Oh s = Big_Oh s1 )
A2: f is eventually-positive

proof

take 1 ; :: according to ASYMPT_0:def 4 :: thesis: for b₁ being set holds
( not 1 <= b₁ or not f . b₁ <= 0 )
let n be Nat; :: thesis: ( not 1 <= n or not f . n <= 0 )
A3: n in NAT by ORDINAL1:def 12;
assume A4: n >= 1 ; :: thesis: not f . n <= 0
then f . n = n to_power (sqrt n) by A1, A3;
hence not f . n <= 0 by A4, POWER:34; :: thesis: verum

end;

set h = f /" (seq_a^ (2,1,0));
reconsider f = f as eventually-positive Real_Sequence by A2;
reconsider g = seq_a^ (2,1,0) as eventually-positive Real_Sequence ;
take f ; :: thesis: ex s1 being eventually-positive Real_Sequence st
( f = f & s1 = seq_a^ (2,1,0) & Big_Oh f c= Big_Oh s1 & not Big_Oh f = Big_Oh s1 )
take g ; :: thesis: ( f = f & g = seq_a^ (2,1,0) & Big_Oh f c= Big_Oh g & not Big_Oh f = Big_Oh g )
consider N being Element of NAT such that
A5: for n being Element of NAT st n >= N holds
n - ((sqrt n) * (log (2,n))) > n / 2 by Lm40;

A6: now :: thesis: for p being Real st p > 0 holds
ex N1 being Nat st
for n being Nat st n >= N1 holds
|.(((f /" (seq_a^ (2,1,0))) . n) - 0).| < p

let p be Real; :: thesis: ( p > 0 implies ex N1 being Nat st
for n being Nat st n >= N1 holds
|.(((f /" (seq_a^ (2,1,0))) . n) - 0).| < p )
assume A7: p > 0 ; :: thesis: ex N1 being Nat st
for n being Nat st n >= N1 holds
|.(((f /" (seq_a^ (2,1,0))) . n) - 0).| < p
set N1 = max (N,(max ((2 * [/(log (2,(1 / p)))\]),2)));
A8: max (N,(max ((2 * [/(log (2,(1 / p)))\]),2))) >= N by XXREAL_0:25;
A9: max (N,(max ((2 * [/(log (2,(1 / p)))\]),2))) is Integer

proof

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

suppose max (N,(max ((2 * [/(log (2,(1 / p)))\]),2))) = N ; :: thesis: max (N,(max ((2 * [/(log (2,(1 / p)))\]),2))) is Integer

hence max (N,(max ((2 * [/(log (2,(1 / p)))\]),2))) is Integer ; :: thesis: verum

end;

suppose max (N,(max ((2 * [/(log (2,(1 / p)))\]),2))) = max ((2 * [/(log (2,(1 / p)))\]),2) ; :: thesis: max (N,(max ((2 * [/(log (2,(1 / p)))\]),2))) is Integer

hence max (N,(max ((2 * [/(log (2,(1 / p)))\]),2))) is Integer by XXREAL_0:16; :: thesis: verum

end;

end;

end;

A10: max (N,(max ((2 * [/(log (2,(1 / p)))\]),2))) >= max ((2 * [/(log (2,(1 / p)))\]),2) by XXREAL_0:25;
max ((2 * [/(log (2,(1 / p)))\]),2) >= 2 * [/(log (2,(1 / p)))\] by XXREAL_0:25;
then A11: max (N,(max ((2 * [/(log (2,(1 / p)))\]),2))) >= 2 * [/(log (2,(1 / p)))\] by A10, XXREAL_0:2;
max (N,(max ((2 * [/(log (2,(1 / p)))\]),2))) in NAT by A8, A9, INT_1:3;
then reconsider N1 = max (N,(max ((2 * [/(log (2,(1 / p)))\]),2))) as Nat ;
take N1 = N1; :: thesis: for n being Nat st n >= N1 holds
|.(((f /" (seq_a^ (2,1,0))) . n) - 0).| < p
let n be Nat; :: thesis: ( n >= N1 implies |.(((f /" (seq_a^ (2,1,0))) . n) - 0).| < p )
A12: n in NAT by ORDINAL1:def 12;
A13: (f /" (seq_a^ (2,1,0))) . n = (f . n) / (g . n) by Lm4;
A14: [/(log (2,(1 / p)))\] >= log (2,(1 / p)) by INT_1:def 7;
assume A15: n >= N1 ; :: thesis: |.(((f /" (seq_a^ (2,1,0))) . n) - 0).| < p
then n >= 2 * [/(log (2,(1 / p)))\] by A11, XXREAL_0:2;
then n / 2 >= [/(log (2,(1 / p)))\] by XREAL_1:77;
then n / 2 >= log (2,(1 / p)) by A14, XXREAL_0:2;
then - (n / 2) <= - (log (2,(1 / p))) by XREAL_1:24;
then 2 to_power (- (n / 2)) <= 2 to_power (- (log (2,(1 / p)))) by PRE_FF:8;
then 2 to_power (- (n / 2)) <= 1 / (2 to_power (log (2,(1 / p)))) by POWER:28;
then A16: 2 to_power (- (n / 2)) <= 1 / (1 / p) by A7, POWER:def 3;
A17: g . n = 2 to_power ((1 * n) + 0) by Def1
.= 2 to_power n ;
A18: max ((2 * [/(log (2,(1 / p)))\]),2) >= 2 by XXREAL_0:25;
then f . n = n to_power (sqrt n) by A1, A10, A15, A12
.= 2 to_power ((sqrt n) * (log (2,n))) by A10, A18, A15, Lm3 ;
then A19: (f /" (seq_a^ (2,1,0))) . n = 2 to_power (((sqrt n) * (log (2,n))) - n) by A13, A17, POWER:29
.= 2 to_power (- (n - ((sqrt n) * (log (2,n))))) ;
then A20: (f /" (seq_a^ (2,1,0))) . n > 0 by POWER:34;
n >= N by A8, A15, XXREAL_0:2;
then n - ((sqrt n) * (log (2,n))) > n / 2 by A5, A12;
then - (n - ((sqrt n) * (log (2,n)))) < - (n / 2) by XREAL_1:24;
then 2 to_power (- (n - ((sqrt n) * (log (2,n))))) < 2 to_power (- (n / 2)) by POWER:39;
then (f /" (seq_a^ (2,1,0))) . n < p by A19, A16, XXREAL_0:2;
hence |.(((f /" (seq_a^ (2,1,0))) . n) - 0).| < p by A20, ABSVALUE:def 1; :: thesis: verum

end;

then A21: f /" (seq_a^ (2,1,0)) is convergent by SEQ_2:def 6;
then A22: lim (f /" (seq_a^ (2,1,0))) = 0 by A6, SEQ_2:def 7;
then not g in Big_Oh f by A21, ASYMPT_0:16;
then A23: not f in Big_Omega g by ASYMPT_0:19;
f in Big_Oh g by A21, A22, ASYMPT_0:16;
hence ( f = f & g = seq_a^ (2,1,0) & Big_Oh f c= Big_Oh g & not Big_Oh f = Big_Oh g ) by A23, Th4; :: thesis: verum