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
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 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 Nat holds seq . n = (1 / (n + r)) * x0 ) holds
seq is convergent
let r be Real; :: thesis: ( 0 < r & ( for n being Nat holds seq . n = (1 / (n + r)) * x0 ) implies seq is convergent )
assume that
A1: 0 < r and
A2: for n being Nat holds seq . n = (1 / (n + r)) * x0 ; :: thesis: seq is convergent
take g = 0. S; :: according to NORMSP_1:def 6 :: thesis: for b₁ being object holds
( b₁ <= 0 or ex b₂ being set st
for b₃ being set holds
( not b₂ <= b₃ or not b₁ <= ||.((seq . b₃) - g).|| ) )
let p be Real; :: thesis: ( p <= 0 or ex b₁ being set st
for b₂ being set holds
( not b₁ <= b₂ or not p <= ||.((seq . b₂) - g).|| ) )
assume A3: 0 < p ; :: thesis: ex b₁ being set st
for b₂ being set 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.|| + 0 < ||.x0.|| + 1 & 0 <= ||.x0.|| ) by NORMSP_1:4, XREAL_1:8;
A5: ||.x0.|| + 1 > 0 + 0 by NORMSP_1:4, XREAL_1:8;
then 0 < p / (||.x0.|| + 1) by A3, XREAL_1:139;
then pp * ||.x0.|| < pp * (||.x0.|| + 1) by A4, XREAL_1:97;
hence ( pp > 0 & pp * ||.x0.|| < p ) by A3, A5, XCMPLX_1:87; :: thesis: verum

end;

then consider pp being Real such that
A6: pp > 0 and
A7: pp * ||.x0.|| < p ;
consider k1 being Nat such that
A8: pp " < k1 by SEQ_4:3;
(pp ") + 0 < k1 + r by A1, A8, XREAL_1:8;
then 1 / (k1 + r) < 1 / (pp ") by A6, XREAL_1:76;
then A9: 1 / (k1 + r) < 1 * ((pp ") ") by XCMPLX_0:def 9;
reconsider k1 = k1 as Element of NAT by ORDINAL1:def 12;
take n = k1; :: thesis: for b₁ being set holds
( not n <= b₁ or not p <= ||.((seq . b₁) - g).|| )
let m be Nat; :: thesis: ( not n <= m or not p <= ||.((seq . m) - g).|| )
assume n <= m ; :: thesis: not p <= ||.((seq . m) - g).||
then A10: n + r <= m + r by XREAL_1:6;
A11: 0 <= ||.x0.|| by NORMSP_1:4;
1 / (m + r) <= 1 / (n + r) by A1, A10, XREAL_1:118;
then 1 / (m + r) < pp by A9, XXREAL_0:2;
then A12: (1 / (m + r)) * ||.x0.|| <= pp * ||.x0.|| by A11, XREAL_1:64;
||.((seq . m) - g).|| = ||.(((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 not p <= ||.((seq . m) - g).|| by A7, A12, XXREAL_0:2; :: thesis: verum