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 NORMSP_1:4, XREAL_1:8;
A7: ||.x0.|| + 1 > 0 + 0 by NORMSP_1:4, XREAL_1:8;
then 0 < p / (||.x0.|| + 1) by A5, XREAL_1:139;
then pp * ||.x0.|| < pp * (||.x0.|| + 1) by A6, XREAL_1:97;
hence ( pp > 0 & pp * ||.x0.|| < p ) by A5, A7, XCMPLX_1:87; :: 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 A1, A10, XREAL_1:8;
then 1 / (k1 + r) < 1 / (pp ") by A8, XREAL_1:76;
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 A1, A12, XREAL_1:118;
then 1 / (m + r) < pp by A11, XXREAL_0:2;
then A13: (1 / (m + r)) * ||.x0.|| <= pp * ||.x0.|| by A4, XREAL_1:64;
||.((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 A1, ABSVALUE:def 1 ;
hence ||.((seq . m) - (0. S)).|| < p by A9, A13, XXREAL_0:2; :: thesis: verum

end;

seq is convergent by A1, A2, Th19;
hence lim seq = 0. S by A3, NORMSP_1:def 7; :: thesis: verum