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:34
.= 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 5;
[/(log 2,(1 / p))\] + 1 > [/(log 2,(1 / p))\] by XREAL_1:31;
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:44;
reconsider N = max 1,([/(log 2,(1 / p))\] + 1) as Element of NAT by A3, A4, INT_1:16;
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:10, 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:10;
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:70;
then A9: p * (2 to_power n) > 1 by A7, XCMPLX_1:88;
2 to_power n > 0 by POWER:39;
then (p * (2 to_power n)) * ((2 to_power n) " ) > 1 * ((2 to_power n) " ) by A9, XREAL_1:70;
then A10: p * ((2 to_power n) * ((2 to_power n) " )) > (2 to_power n) " ;
2 to_power n <> 0 by POWER:39;
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:39;
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:33; :: 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