reconsider f = seq_a^ 2,1,0 as eventually-positive Real_Sequence ;
reconsider g = seq_a^ 2,2,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 )
assume A3: 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
then p " > 0 ;
then A4: 1 / p > 0 ;
set N = max 1,([/(log 2,(1 / p))\] + 1);
A5: ( max 1,([/(log 2,(1 / p))\] + 1) >= 1 & max 1,([/(log 2,(1 / p))\] + 1) >= [/(log 2,(1 / p))\] + 1 ) by XXREAL_0:25;
max 1,([/(log 2,(1 / p))\] + 1) is Integer by XXREAL_0:16;
then reconsider N = max 1,([/(log 2,(1 / p))\] + 1) as Element of NAT by A5, INT_1:16;
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 )
assume A6: n >= N ; :: thesis: abs (((f /" g) . n) - 0 ) < p
A7: abs (((f /" g) . n) - 0 ) = abs (2 to_power (- n)) by A1;
2 to_power (- n) > 0 by POWER:39;
then A8: abs (((f /" g) . n) - 0 ) = 2 to_power (- n) by A7, ABSVALUE:def 1;
A9: 2 to_power n >= 2 to_power N by A6, PRE_FF:10;
A10: 2 to_power N >= 2 to_power ([/(log 2,(1 / p))\] + 1) by PRE_FF:10, XXREAL_0:25;
A11: [/(log 2,(1 / p))\] + 1 > [/(log 2,(1 / p))\] by XREAL_1:31;
[/(log 2,(1 / p))\] >= log 2,(1 / p) by INT_1:def 5;
then [/(log 2,(1 / p))\] + 1 > log 2,(1 / p) by A11, XXREAL_0:2;
then 2 to_power ([/(log 2,(1 / p))\] + 1) > 2 to_power (log 2,(1 / p)) by POWER:44;
then 2 to_power N > 2 to_power (log 2,(1 / p)) by A10, XXREAL_0:2;
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 A4, POWER:def 3;
then (2 to_power n) * p > (1 / p) * p by A3, XREAL_1:70;
then A12: p * (2 to_power n) > 1 by A3, XCMPLX_1:88;
2 to_power n > 0 by POWER:39;
then (2 to_power n) " > 0 ;
then (p * (2 to_power n)) * ((2 to_power n) " ) > 1 * ((2 to_power n) " ) by A12, XREAL_1:70;
then A13: 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 A13, XCMPLX_0:def 7;
then p > 1 / (2 to_power n) ;
hence abs (((f /" g) . n) - 0 ) < p by A8, POWER:33; :: thesis: verum

end;

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