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 Element of NAT holds seq . n = (1 / (n + r)) * x0 ) holds
seq is convergent
let seq be sequence of S; :: thesis: for x0 being Point of S
for r being Real st 0 < r & ( for n being Element of NAT holds seq . n = (1 / (n + r)) * x0 ) holds
seq is convergent
let x0 be Point of S; :: thesis: for r being Real st 0 < r & ( for n being Element of NAT holds seq . n = (1 / (n + r)) * x0 ) holds
seq is convergent
let r be Real; :: thesis: ( 0 < r & ( for n being Element of NAT holds seq . n = (1 / (n + r)) * x0 ) implies seq is convergent )
assume that
A1: 0 < r and
A2: for n being Element of NAT holds seq . n = (1 / (n + r)) * x0 ; :: thesis: seq is convergent
take g = 0. S; :: according to NORMSP_1:def 9 :: thesis: for b₁ being Element of REAL holds
( b₁ <= 0 or ex b₂ being Element of NAT st
for b₃ being Element of NAT holds
( not b₂ <= b₃ or not b₁ <= ||.((seq . b₃) - g).|| ) )
let p be Real; :: thesis: ( p <= 0 or ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not p <= ||.((seq . b₂) - g).|| ) )
assume A3: 0 < p ; :: thesis: ex b₁ being Element of NAT st
for b₂ being Element of NAT holds
( not b₁ <= b₂ or not p <= ||.((seq . b₂) - g).|| )
ex pp being Real st
( pp > 0 & pp * ||.x0.|| < p )

proof

take pp = p / (||.x0.|| + 1); :: thesis: ( pp > 0 & pp * ||.x0.|| < p )
A4: ||.x0.|| + 1 > 0 + 0 by NORMSP_1:8, XREAL_1:10;
then A5: 0 < p / (||.x0.|| + 1) by A3, XREAL_1:141;
A6: ||.x0.|| + 0 < ||.x0.|| + 1 by XREAL_1:10;
0 <= ||.x0.|| by NORMSP_1:8;
then pp * ||.x0.|| < pp * (||.x0.|| + 1) by A5, A6, XREAL_1:99;
hence ( pp > 0 & pp * ||.x0.|| < p ) by A3, A4, XCMPLX_1:88; :: thesis: verum

end;

then consider pp being Real such that
A7: ( pp > 0 & pp * ||.x0.|| < p ) ;
A8: 0 < pp " by A7;
consider k1 being Element of NAT such that
A9: pp " < k1 by SEQ_4:10;
take n = k1; :: thesis: for b₁ being Element of NAT holds
( not n <= b₁ or not p <= ||.((seq . b₁) - g).|| )
let m be Element of NAT ; :: thesis: ( not n <= m or not p <= ||.((seq . m) - g).|| )
assume A10: n <= m ; :: thesis: not p <= ||.((seq . m) - g).||
(pp " ) + 0 < k1 + r by A1, A9, XREAL_1:10;
then 1 / (k1 + r) < 1 / (pp " ) by A8, XREAL_1:78;
then A11: 1 / (k1 + r) < 1 * ((pp " ) " ) by XCMPLX_0:def 9;
A12: 0 + 0 < n + r by A1, A8, A9;
n + r <= m + r by A10, XREAL_1:8;
then 1 / (m + r) <= 1 / (n + r) by A12, XREAL_1:120;
then A13: 1 / (m + r) < pp by A11, XXREAL_0:2;
0 <= m by NAT_1:2;
then 0 + 0 < m + r by A1;
then A14: 0 / (m + r) < 1 / (m + r) by XREAL_1:76;
A15: ||.((seq . m) - g).|| = ||.(((1 / (m + r)) * x0) - (0. S)).|| by A2
.= ||.((1 / (m + r)) * x0).|| by RLVECT_1:26
.= (abs (1 / (m + r))) * ||.x0.|| by NORMSP_1:def 2
.= (1 / (m + r)) * ||.x0.|| by A14, ABSVALUE:def 1 ;
0 <= ||.x0.|| by NORMSP_1:8;
then (1 / (m + r)) * ||.x0.|| <= pp * ||.x0.|| by A13, XREAL_1:66;
hence not p <= ||.((seq . m) - g).|| by A7, A15, XXREAL_0:2; :: thesis: verum