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: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 )
A6: [/(9 + (log 2,(1 / p)))\] >= 9 + (log 2,(1 / p)) by INT_1:def 5;
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: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 A8: 1 / (2 to_power (n - 9)) <= 1 / (1 / p) by A2, XREAL_1:87;
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