let r be real number ; :: thesis: for seq being Real_Sequence st 0 <= r & ( for n being Element of NAT holds seq . n = 1 / ((n * n) + r) ) holds
lim seq = 0
let seq be Real_Sequence; :: thesis: ( 0 <= r & ( for n being Element of NAT holds seq . n = 1 / ((n * n) + r) ) implies lim seq = 0 )
assume that
A1: 0 <= r and
A2: for n being Element of NAT holds seq . n = 1 / ((n * n) + r) ; :: thesis: lim seq = 0

A3: now

let p be real number ; :: thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - 0) < p )
consider k1 being Element of NAT such that
A4: p " < k1 by Th10;
assume A5: 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - 0) < p
then A6: k1 > 0 by A4;
then k1 >= 1 + 0 by NAT_1:13;
then k1 <= k1 * k1 by XREAL_1:151;
then A7: k1 + r <= (k1 * k1) + r by XREAL_1:6;
take n = k1; :: thesis: for m being Element of NAT st n <= m holds
abs ((seq . m) - 0) < p
let m be Element of NAT ; :: thesis: ( n <= m implies abs ((seq . m) - 0) < p )
assume n <= m ; :: thesis: abs ((seq . m) - 0) < p
then n * n <= m * m by XREAL_1:66;
then A8: (n * n) + r <= (m * m) + r by XREAL_1:6;
(p ") + 0 < k1 + r by A1, A4, XREAL_1:8;
then (p ") + 0 < (k1 * k1) + r by A7, XXREAL_0:2;
then 1 / ((k1 * k1) + r) < 1 / (p ") by A5, XREAL_1:76;
then A9: 1 / ((k1 * k1) + r) < 1 * ((p ") ") by XCMPLX_0:def 9;
0 < n ^2 by A6, SQUARE_1:12;
then 1 / ((m * m) + r) <= 1 / ((n * n) + r) by A1, A8, XREAL_1:118;
then A10: 1 / ((m * m) + r) < p by A9, XXREAL_0:2;
( seq . m = 1 / ((m * m) + r) & 0 <= m * m ) by A2;
hence abs ((seq . m) - 0) < p by A1, A10, ABSVALUE:def 1; :: thesis: verum

end;

seq is convergent by A1, A2, Th47;
hence lim seq = 0 by A3, SEQ_2:def 7; :: thesis: verum