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 :: thesis: for p being Real st p > 0 holds
ex N being Nat st
for n being Nat st n >= N holds
|.(((f /" (seq_n! 0)) . n) - 0).| < p

let p be Real; :: thesis: ( p > 0 implies ex N being Nat st
for n being Nat st n >= N holds
|.(((f /" (seq_n! 0)) . n) - 0).| < p )
assume A2: p > 0 ; :: thesis: ex N being Nat st
for n being Nat st n >= N holds
|.(((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;
max (10,[/(9 + (log (2,(1 / p))))\]) in NAT by A3, A4, INT_1:3;
then reconsider N = max (10,[/(9 + (log (2,(1 / p))))\]) as Nat ;
take N = N; :: thesis: for n being Nat st n >= N holds
|.(((f /" (seq_n! 0)) . n) - 0).| < p
let n be Nat; :: thesis: ( n >= N implies |.(((f /" (seq_n! 0)) . n) - 0).| < p )
A6: n in NAT by ORDINAL1:def 12;
A7: [/(9 + (log (2,(1 / p))))\] >= 9 + (log (2,(1 / p))) by INT_1:def 7;
assume A8: n >= N ; :: thesis: |.(((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 A7, 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 A9: 1 / (2 to_power (n - 9)) <= 1 / (1 / p) by A2, XREAL_1:85;
A10: (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, A6
.= (2 to_power ((2 * n) + 0)) / ((n + 0) !) by Def4
.= (2 to_power (2 * n)) / (n !) ;
n >= 10 by A3, A8, XXREAL_0:2;
then (f /" (seq_n! 0)) . n < 1 / (2 to_power (n - 9)) by A10, Lm34, A6;
then (f /" (seq_n! 0)) . n < p by A9, XXREAL_0:2;
hence |.(((f /" (seq_n! 0)) . n) - 0).| < p by A10, ABSVALUE:def 1; :: thesis: verum

end;

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