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.|| is convergent & lim ||.seq.|| = ||.g.|| )

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

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

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

assume that

A1: seq is convergent and

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

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

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

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

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

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

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

assume that

A1: seq is convergent and

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

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

ex k being Nat st

for n being Nat st k <= n holds

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

||.seq.|| is convergent
by A1, Th20;ex k being Nat st

for n being Nat st k <= n holds

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

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

for n being Nat st k <= n holds

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

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

for n being Nat st k <= n holds

|.((||.seq.|| . n) - ||.g.||).| < 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 k <= n holds

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

|.((||.seq.|| . n) - ||.g.||).| < r ; :: thesis: verum

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

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

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

for n being Nat st k <= n holds

|.((||.seq.|| . n) - ||.g.||).| < 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 k <= n holds

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

now :: thesis: for n being Nat st n >= k holds

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

hence
for n being Nat st k <= n holds |.((||.seq.|| . n) - ||.g.||).| < r

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

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

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

|.(||.(seq . n).|| - ||.g.||).| <= ||.((seq . n) - g).|| by BHSP_1:33;

then |.(||.(seq . n).|| - ||.g.||).| < r by A6, XXREAL_0:2;

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

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

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

|.(||.(seq . n).|| - ||.g.||).| <= ||.((seq . n) - g).|| by BHSP_1:33;

then |.(||.(seq . n).|| - ||.g.||).| < r by A6, XXREAL_0:2;

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

|.((||.seq.|| . n) - ||.g.||).| < r ; :: thesis: verum

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