set g = seq_n! 0 ;
reconsider f = seq_a^ 2,2,0 as eventually-positive Real_Sequence ;
take f ; :: thesis: ( f = seq_a^ 2,2,0 & Big_Oh f c= Big_Oh (seq_n! 0 ) & not Big_Oh f = Big_Oh (seq_n! 0 ) )
thus f = seq_a^ 2,2,0 ; :: thesis: ( Big_Oh f c= Big_Oh (seq_n! 0 ) & not Big_Oh f = Big_Oh (seq_n! 0 ) )
set h = f /" (seq_n! 0 );

A1: 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 /" (seq_n! 0 )) . n) - 0 ) < p )
assume p > 0 ; :: thesis: ex N being Element of NAT st
for n being Element of NAT st n >= N holds
abs (((f /" (seq_n! 0 )) . n) - 0 ) < p
then p " > 0 ;
then A2: 1 / p > 0 ;
set N = max 10,[/(9 + (log 2,(1 / p)))\];
A3: ( max 10,[/(9 + (log 2,(1 / p)))\] >= 10 & max 10,[/(9 + (log 2,(1 / p)))\] >= [/(9 + (log 2,(1 / p)))\] ) by XXREAL_0:25;
max 10,[/(9 + (log 2,(1 / p)))\] is Integer by XXREAL_0:16;
then reconsider N = max 10,[/(9 + (log 2,(1 / p)))\] as Element of NAT by A3, INT_1:16;
take N = N; :: thesis: for n being Element of NAT st n >= N holds
abs (((f /" (seq_n! 0 )) . n) - 0 ) < p
let n be Element of NAT ; :: thesis: ( n >= N implies abs (((f /" (seq_n! 0 )) . n) - 0 ) < p )
assume n >= N ; :: thesis: abs (((f /" (seq_n! 0 )) . n) - 0 ) < p
then A4: ( n >= 10 & n >= [/(9 + (log 2,(1 / p)))\] ) by A3, XXREAL_0:2;
A5: (f /" (seq_n! 0 )) . n = (f . n) / ((seq_n! 0 ) . n) by Lm4
.= (2 to_power ((2 * n) + 0 )) / ((seq_n! 0 ) . n) by Def1
.= (2 to_power ((2 * n) + 0 )) / ((n + 0 ) ! ) by Def5
.= (2 to_power (2 * n)) / (n ! ) ;
then A6: (f /" (seq_n! 0 )) . n < 1 / (2 to_power (n - 9)) by A4, Lm40;
[/(9 + (log 2,(1 / p)))\] >= 9 + (log 2,(1 / p)) by INT_1:def 5;
then n >= 9 + (log 2,(1 / p)) by A4, XXREAL_0:2;
then n - 9 >= log 2,(1 / p) by XREAL_1:21;
then 2 to_power (n - 9) >= 2 to_power (log 2,(1 / p)) by PRE_FF:10;
then 2 to_power (n - 9) >= 1 / p by A2, POWER:def 3;
then 1 / (2 to_power (n - 9)) <= 1 / (1 / p) by A2, XREAL_1:87;
then 1 / (2 to_power (n - 9)) <= p ;
then (f /" (seq_n! 0 )) . n < p by A6, XXREAL_0:2;
hence abs (((f /" (seq_n! 0 )) . n) - 0 ) < p by A5, ABSVALUE:def 1; :: thesis: verum

end;

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