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

let p be real number ; :: thesis: ( p > 0 implies ex N being Element of NAT st
for n being Element of NAT st n >= N holds
abs (((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;
reconsider N = max (1,([/(log (2,(1 / p)))\] + 1)) as Element of NAT by A3, A4, INT_1:3;
assume A7: p > 0 ; :: thesis: ex N being Element of NAT st
for n being Element of NAT st n >= N holds
abs (((f /" g) . n) - 0) < p
take N = N; :: thesis: for n being Element of NAT st n >= N holds
abs (((f /" g) . n) - 0) < p
let n be Element of NAT ; :: thesis: ( n >= N implies abs (((f /" g) . n) - 0) < p )
2 to_power N >= 2 to_power ([/(log (2,(1 / p)))\] + 1) by PRE_FF:8, XXREAL_0:25;
then A8: 2 to_power N > 2 to_power (log (2,(1 / p))) by A6, XXREAL_0:2;
assume n >= N ; :: thesis: abs (((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 A8, 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 A9: 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 A9, XREAL_1:68;
then A10: 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 A10, XCMPLX_0:def 7;
then A11: p > 1 / (2 to_power n) ;
A12: 2 to_power (- n) > 0 by POWER:34;
abs (((f /" g) . n) - 0) = abs (2 to_power (- n)) by A1;
then abs (((f /" g) . n) - 0) = 2 to_power (- n) by A12, ABSVALUE:def 1;
hence abs (((f /" g) . n) - 0) < p by A11, POWER:28; :: thesis: verum

end;

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