reconsider f = seq_a^ (2,2,0) as eventually-positive Real_Sequence ;
set g = seq_n! 0;
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 A2: 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
set N = max (10,[/(9 + (log (2,(1 / p))))\]);
A3: max (10,[/(9 + (log (2,(1 / p))))\]) >= 10 by XXREAL_0:25;
A4: max (10,[/(9 + (log (2,(1 / p))))\]) is Integer by XXREAL_0:16;
A5: max (10,[/(9 + (log (2,(1 / p))))\]) >= [/(9 + (log (2,(1 / p))))\] by XXREAL_0:25;
reconsider N = max (10,[/(9 + (log (2,(1 / p))))\]) as Element of NAT by A3, A4, INT_1:3;
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 )
A6: [/(9 + (log (2,(1 / p))))\] >= 9 + (log (2,(1 / p))) by INT_1:def 7;
assume A7: n >= N ; :: thesis: abs (((f /" (seq_n! 0)) . n) - 0) < p
then n >= [/(9 + (log (2,(1 / p))))\] by A5, XXREAL_0:2;
then n >= 9 + (log (2,(1 / p))) by A6, XXREAL_0:2;
then n - 9 >= log (2,(1 / p)) by XREAL_1:19;
then 2 to_power (n - 9) >= 2 to_power (log (2,(1 / p))) by PRE_FF:8;
then 2 to_power (n - 9) >= 1 / p by A2, POWER:def 3;
then A8: 1 / (2 to_power (n - 9)) <= 1 / (1 / p) by A2, XREAL_1:85;
A9: (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 !) ;
n >= 10 by A3, A7, XXREAL_0:2;
then (f /" (seq_n! 0)) . n < 1 / (2 to_power (n - 9)) by A9, Lm34;
then (f /" (seq_n! 0)) . n < p by A8, XXREAL_0:2;
hence abs (((f /" (seq_n! 0)) . n) - 0) < p by A9, ABSVALUE:def 1; :: thesis: verum

end;

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