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

hence lim seq = 0. S by A3, NORMSP_1:def 7; :: 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

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

seq is convergent
by A1, A2, Th19;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 )

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;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

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

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

hence lim seq = 0. S by A3, NORMSP_1:def 7; :: thesis: verum