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 + r) ) holds
lim seq = 0
let seq be Real_Sequence; :: thesis: ( 0 <= r & ( for n being Element of NAT holds seq . n = 1 / (n + r) ) implies lim seq = 0 )
assume that
A1: 0 <= r and
A2: for n being Element of NAT holds seq . n = 1 / (n + r) ; :: thesis: lim seq = 0
A3: seq is convergent by A1, A2, Th43;

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 )
assume 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 A4: 0 < p " ;
consider k1 being Element of NAT such that
A5: p " < k1 by Th10;
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 A6: n <= m ; :: thesis: abs ((seq . m) - 0 ) < p
(p " ) + 0 < k1 + r by A1, A5, XREAL_1:10;
then 1 / (k1 + r) < 1 / (p " ) by A4, XREAL_1:78;
then A7: 1 / (k1 + r) < 1 * ((p " ) " ) by XCMPLX_0:def 9;
n + r <= m + r by A6, XREAL_1:8;
then 1 / (m + r) <= 1 / (n + r) by A1, A4, A5, XREAL_1:120;
then A9: 1 / (m + r) < p by A7, XXREAL_0:2;
A10: seq . m = 1 / (m + r) by A2;
0 <= m by NAT_1:2;
hence abs ((seq . m) - 0 ) < p by A9, A10, A1, ABSVALUE:def 1; :: thesis: verum

end;

hence lim seq = 0 by A3, SEQ_2:def 7; :: thesis: verum