let X be RealUnitarySpace; :: thesis: for g being Point of X

for seq being sequence of X st seq is convergent & lim seq = g holds

( ||.(seq - g).|| is convergent & lim ||.(seq - g).|| = 0 )

let g be Point of X; :: thesis: for seq being sequence of X st seq is convergent & lim seq = g holds

( ||.(seq - g).|| is convergent & lim ||.(seq - g).|| = 0 )

let seq be sequence of X; :: thesis: ( seq is convergent & lim seq = g implies ( ||.(seq - g).|| is convergent & lim ||.(seq - g).|| = 0 ) )

assume that

A1: seq is convergent and

A2: lim seq = g ; :: thesis: ( ||.(seq - g).|| is convergent & lim ||.(seq - g).|| = 0 )

hence ( ||.(seq - g).|| is convergent & lim ||.(seq - g).|| = 0 ) by A3, SEQ_2:def 7; :: thesis: verum

for seq being sequence of X st seq is convergent & lim seq = g holds

( ||.(seq - g).|| is convergent & lim ||.(seq - g).|| = 0 )

let g be Point of X; :: thesis: for seq being sequence of X st seq is convergent & lim seq = g holds

( ||.(seq - g).|| is convergent & lim ||.(seq - g).|| = 0 )

let seq be sequence of X; :: thesis: ( seq is convergent & lim seq = g implies ( ||.(seq - g).|| is convergent & lim ||.(seq - g).|| = 0 ) )

assume that

A1: seq is convergent and

A2: lim seq = g ; :: thesis: ( ||.(seq - g).|| is convergent & lim ||.(seq - g).|| = 0 )

A3: now :: thesis: for r being Real st r > 0 holds

ex k being Nat st

for n being Nat st n >= k holds

|.((||.(seq - g).|| . n) - 0).| < r

||.(seq - g).|| is convergent
by A1, Th8, Th20;ex k being Nat st

for n being Nat st n >= k holds

|.((||.(seq - g).|| . n) - 0).| < r

let r be Real; :: thesis: ( r > 0 implies ex k being Nat st

for n being Nat st n >= k holds

|.((||.(seq - g).|| . n) - 0).| < r )

assume A4: r > 0 ; :: thesis: ex k being Nat st

for n being Nat st n >= k holds

|.((||.(seq - g).|| . n) - 0).| < r

consider m1 being Nat such that

A5: for n being Nat st n >= m1 holds

||.((seq . n) - g).|| < r by A1, A2, A4, Th19;

reconsider k = m1 as Nat ;

take k = k; :: thesis: for n being Nat st n >= k holds

|.((||.(seq - g).|| . n) - 0).| < r

let n be Nat; :: thesis: ( n >= k implies |.((||.(seq - g).|| . n) - 0).| < r )

assume n >= k ; :: thesis: |.((||.(seq - g).|| . n) - 0).| < r

then ||.((seq . n) - g).|| < r by A5;

then A6: ||.(((seq . n) - g) - H_{1}(X)).|| < r
by RLVECT_1:13;

|.(||.((seq . n) - g).|| - ||.H_{1}(X).||).| <= ||.(((seq . n) - g) - H_{1}(X)).||
by BHSP_1:33;

then |.(||.((seq . n) - g).|| - ||.H_{1}(X).||).| < r
by A6, XXREAL_0:2;

then |.(||.((seq . n) - g).|| - 0).| < r by BHSP_1:26;

then |.(||.((seq - g) . n).|| - 0).| < r by NORMSP_1:def 4;

hence |.((||.(seq - g).|| . n) - 0).| < r by Def3; :: thesis: verum

end;for n being Nat st n >= k holds

|.((||.(seq - g).|| . n) - 0).| < r )

assume A4: r > 0 ; :: thesis: ex k being Nat st

for n being Nat st n >= k holds

|.((||.(seq - g).|| . n) - 0).| < r

consider m1 being Nat such that

A5: for n being Nat st n >= m1 holds

||.((seq . n) - g).|| < r by A1, A2, A4, Th19;

reconsider k = m1 as Nat ;

take k = k; :: thesis: for n being Nat st n >= k holds

|.((||.(seq - g).|| . n) - 0).| < r

let n be Nat; :: thesis: ( n >= k implies |.((||.(seq - g).|| . n) - 0).| < r )

assume n >= k ; :: thesis: |.((||.(seq - g).|| . n) - 0).| < r

then ||.((seq . n) - g).|| < r by A5;

then A6: ||.(((seq . n) - g) - H

|.(||.((seq . n) - g).|| - ||.H

then |.(||.((seq . n) - g).|| - ||.H

then |.(||.((seq . n) - g).|| - 0).| < r by BHSP_1:26;

then |.(||.((seq - g) . n).|| - 0).| < r by NORMSP_1:def 4;

hence |.((||.(seq - g).|| . n) - 0).| < r by Def3; :: thesis: verum

hence ( ||.(seq - g).|| is convergent & lim ||.(seq - g).|| = 0 ) by A3, SEQ_2:def 7; :: thesis: verum