reconsider g = seq_a^ (2,2,0) as eventually-positive Real_Sequence ;
reconsider f = seq_a^ (2,1,0) as eventually-positive Real_Sequence ;
take f ; :: thesis: ex s1 being eventually-positive Real_Sequence st
( f = seq_a^ (2,1,0) & s1 = seq_a^ (2,2,0) & Big_Oh f c= Big_Oh s1 & not Big_Oh f = Big_Oh s1 )
take g ; :: thesis: ( f = seq_a^ (2,1,0) & g = seq_a^ (2,2,0) & Big_Oh f c= Big_Oh g & not Big_Oh f = Big_Oh g )
thus ( f = seq_a^ (2,1,0) & g = seq_a^ (2,2,0) ) ; :: thesis: ( Big_Oh f c= Big_Oh g & not Big_Oh f = Big_Oh g )
set h = f /" g;
A1: for n being Element of NAT holds (f /" g) . n = 2 to_power (- n)

proof

let n be Element of NAT ; :: thesis: (f /" g) . n = 2 to_power (- n)
(f /" g) . n = (f . n) / (g . n) by Lm4
.= (2 to_power ((1 * n) + 0)) / (g . n) by Def1
.= (2 to_power (1 * n)) / (2 to_power ((2 * n) + 0)) by Def1
.= 2 to_power ((1 * n) - (2 * n)) by POWER:29
.= 2 to_power (- n) ;
hence (f /" g) . n = 2 to_power (- n) ; :: thesis: verum

end;

A2: now :: thesis: for p being Real st p > 0 holds
ex N being Nat st
for n being Nat st n >= N holds
|.(((f /" g) . n) - 0).| < p

let p be Real; :: thesis: ( p > 0 implies ex N being Nat st
for n being Nat st n >= N holds
|.(((f /" g) . n) - 0).| < p )
set N = max (1,([/(log (2,(1 / p)))\] + 1));
A3: max (1,([/(log (2,(1 / p)))\] + 1)) >= 1 by XXREAL_0:25;
A4: max (1,([/(log (2,(1 / p)))\] + 1)) is Integer by XXREAL_0:16;
A5: [/(log (2,(1 / p)))\] >= log (2,(1 / p)) by INT_1:def 7;
[/(log (2,(1 / p)))\] + 1 > [/(log (2,(1 / p)))\] by XREAL_1:29;
then [/(log (2,(1 / p)))\] + 1 > log (2,(1 / p)) by A5, XXREAL_0:2;
then A6: 2 to_power ([/(log (2,(1 / p)))\] + 1) > 2 to_power (log (2,(1 / p))) by POWER:39;
max (1,([/(log (2,(1 / p)))\] + 1)) in NAT by A3, A4, INT_1:3;
then reconsider N = max (1,([/(log (2,(1 / p)))\] + 1)) as Nat ;
assume A7: p > 0 ; :: thesis: ex N being Nat st
for n being Nat st n >= N holds
|.(((f /" g) . n) - 0).| < p
take N = N; :: thesis: for n being Nat st n >= N holds
|.(((f /" g) . n) - 0).| < p
let n be Nat; :: thesis: ( n >= N implies |.(((f /" g) . n) - 0).| < p )
A8: n in NAT by ORDINAL1:def 12;
[/(log (2,(1 / p)))\] + 1 <= N by XXREAL_0:25;
then 2 to_power N >= 2 to_power ([/(log (2,(1 / p)))\] + 1) by PRE_FF:8;
then A9: 2 to_power N > 2 to_power (log (2,(1 / p))) by A6, XXREAL_0:2;
assume n >= N ; :: thesis: |.(((f /" g) . n) - 0).| < p
then 2 to_power n >= 2 to_power N by PRE_FF:8;
then 2 to_power n > 2 to_power (log (2,(1 / p))) by A9, XXREAL_0:2;
then 2 to_power n > 1 / p by A7, POWER:def 3;
then (2 to_power n) * p > (1 / p) * p by A7, XREAL_1:68;
then A10: p * (2 to_power n) > 1 by A7, XCMPLX_1:87;
2 to_power n > 0 by POWER:34;
then (p * (2 to_power n)) * ((2 to_power n) ") > 1 * ((2 to_power n) ") by A10, XREAL_1:68;
then A11: p * ((2 to_power n) * ((2 to_power n) ")) > (2 to_power n) " ;
2 to_power n <> 0 by POWER:34;
then p * 1 > (2 to_power n) " by A11, XCMPLX_0:def 7;
then A12: p > 1 / (2 to_power n) ;
A13: 2 to_power (- n) > 0 by POWER:34;
|.(((f /" g) . n) - 0).| = |.(2 to_power (- n)).| by A1, A8;
then |.(((f /" g) . n) - 0).| = 2 to_power (- n) by A13, ABSVALUE:def 1;
hence |.(((f /" g) . n) - 0).| < p by A12, POWER:28; :: thesis: verum

end;

then A14: f /" g is convergent by SEQ_2:def 6;
then A15: lim (f /" g) = 0 by A2, SEQ_2:def 7;
then not g in Big_Oh f by A14, ASYMPT_0:16;
then A16: not f in Big_Omega g by ASYMPT_0:19;
f in Big_Oh g by A14, A15, ASYMPT_0:16;
hence ( Big_Oh f c= Big_Oh g & not Big_Oh f = Big_Oh g ) by A16, Th4; :: thesis: verum