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