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_{1} being object holds

( b_{1} <= 0 or ex b_{2} being set st

for b_{3} being set holds

( not b_{2} <= b_{3} or not b_{1} <= ||.((seq . b_{3}) - g).|| ) )

let p be Real; :: thesis: ( p <= 0 or ex b_{1} being set st

for b_{2} being set holds

( not b_{1} <= b_{2} or not p <= ||.((seq . b_{2}) - g).|| ) )

assume A3: 0 < p ; :: thesis: ex b_{1} being set st

for b_{2} being set holds

( not b_{1} <= b_{2} or not p <= ||.((seq . b_{2}) - g).|| )

ex pp being Real st

( pp > 0 & pp * ||.x0.|| < p )

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_{1} being set holds

( not n <= b_{1} or not p <= ||.((seq . b_{1}) - 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

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

( b

for b

( not b

let p be Real; :: thesis: ( p <= 0 or ex b

for b

( not b

assume A3: 0 < p ; :: thesis: ex b

for b

( not b

ex pp being Real st

( pp > 0 & pp * ||.x0.|| < p )

proof

then consider pp being Real such that
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;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

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

( not n <= b

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