let r be Real; :: thesis: for seq being Real_Sequence st 0 <= r & ( for n being Nat holds seq . n = 1 / (n + r) ) holds
lim seq = 0
let seq be Real_Sequence; :: thesis: ( 0 <= r & ( for n being Nat holds seq . n = 1 / (n + r) ) implies lim seq = 0 )
assume that
A1: 0 <= r and
A2: for n being Nat holds seq . n = 1 / (n + r) ; :: thesis: lim seq = 0

A3: now :: thesis: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - 0).| < p

let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - 0).| < p )
assume A4: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - 0).| < p
consider k1 being Nat such that
A5: p " < k1 by Th3;
(p ") + 0 < k1 + r by A1, A5, XREAL_1:8;
then 1 / (k1 + r) < 1 / (p ") by A4, XREAL_1:76;
then A6: 1 / (k1 + r) < 1 * ((p ") ") by XCMPLX_0:def 9;
take n = k1; :: thesis: for m being Nat st n <= m holds
|.((seq . m) - 0).| < p
let m be Nat; :: thesis: ( n <= m implies |.((seq . m) - 0).| < p )
assume n <= m ; :: thesis: |.((seq . m) - 0).| < p
then A7: n + r <= m + r by XREAL_1:6;
0 < p " by A4;
then 1 / (m + r) <= 1 / (n + r) by A1, A5, A7, XREAL_1:118;
then A8: 1 / (m + r) < p by A6, XXREAL_0:2;
( seq . m = 1 / (m + r) & 0 <= m ) by A2;
hence |.((seq . m) - 0).| < p by A1, A8, ABSVALUE:def 1; :: thesis: verum

end;

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