let S be RealNormSpace; :: thesis: for seq being sequence of S
for x0 being Point of S
for r being Real st 0 < r & ( for n being Nat holds seq . n = (1 / (n + r)) * x0 ) holds
lim seq = 0. S

let seq be sequence of S; :: thesis: for x0 being Point of S
for r being Real st 0 < r & ( for n being Nat holds seq . n = (1 / (n + r)) * x0 ) holds
lim seq = 0. S

let x0 be Point of S; :: thesis: for r being Real st 0 < r & ( for n being Nat holds seq . n = (1 / (n + r)) * x0 ) holds
lim seq = 0. S

let r be Real; :: thesis: ( 0 < r & ( for n being Nat holds seq . n = (1 / (n + r)) * x0 ) implies lim seq = 0. S )
assume that
A1: 0 < r and
A2: for n being Nat holds seq . n = (1 / (n + r)) * x0 ; :: thesis: lim seq = 0. S
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. S)).|| < 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. S)).|| < p )

A4: 0 <= ||.x0.|| by NORMSP_1:4;
assume A5: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
||.((seq . m) - (0. S)).|| < p

ex pp being Real st
( pp > 0 & pp * ||.x0.|| < p )
proof
take pp = p / (||.x0.|| + 1); :: thesis: ( pp > 0 & pp * ||.x0.|| < p )
A6: ( ||.x0.|| + 0 < ||.x0.|| + 1 & 0 <= ||.x0.|| ) by ;
A7: ||.x0.|| + 1 > 0 + 0 by ;
then 0 < p / (||.x0.|| + 1) by ;
then pp * ||.x0.|| < pp * (||.x0.|| + 1) by ;
hence ( pp > 0 & pp * ||.x0.|| < p ) by ; :: thesis: verum
end;
then consider pp being Real such that
A8: pp > 0 and
A9: pp * ||.x0.|| < p ;
consider k1 being Nat such that
A10: pp " < k1 by SEQ_4:3;
(pp ") + 0 < k1 + r by ;
then 1 / (k1 + r) < 1 / (pp ") by ;
then A11: 1 / (k1 + r) < 1 * ((pp ") ") by XCMPLX_0:def 9;
reconsider n = k1 as Nat ;
take n = n; :: thesis: for m being Nat st n <= m holds
||.((seq . m) - (0. S)).|| < p

let m be Nat; :: thesis: ( n <= m implies ||.((seq . m) - (0. S)).|| < p )
assume n <= m ; :: thesis: ||.((seq . m) - (0. S)).|| < p
then A12: n + r <= m + r by XREAL_1:6;
1 / (m + r) <= 1 / (n + r) by ;
then 1 / (m + r) < pp by ;
then A13: (1 / (m + r)) * ||.x0.|| <= pp * ||.x0.|| by ;
||.((seq . m) - (0. S)).|| = ||.(((1 / (m + r)) * x0) - (0. S)).|| by A2
.= ||.((1 / (m + r)) * x0).|| by RLVECT_1:13
.= |.(1 / (m + r)).| * ||.x0.|| by NORMSP_1:def 1
.= (1 / (m + r)) * ||.x0.|| by ;
hence ||.((seq . m) - (0. S)).|| < p by ; :: thesis: verum
end;
seq is convergent by A1, A2, Th19;
hence lim seq = 0. S by ; :: thesis: verum