let X be RealUnitarySpace; :: thesis: for seq being sequence of X st seq is convergent holds

||.seq.|| is convergent

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

assume seq is convergent ; :: thesis: ||.seq.|| is convergent

then consider g being Point of X such that

A1: for r being Real st r > 0 holds

ex m being Nat st

for n being Nat st n >= m holds

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

||.seq.|| is convergent

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

assume seq is convergent ; :: thesis: ||.seq.|| is convergent

then consider g being Point of X such that

A1: for r being Real st r > 0 holds

ex m being Nat st

for n being Nat st n >= m holds

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

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

hence
||.seq.|| is convergent
by SEQ_2:def 6; :: thesis: verumex 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 A2: 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

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

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

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 A2: 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

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

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

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 A4: ||.((seq . n) - g).|| < r by A3;

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

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

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

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

then A4: ||.((seq . n) - g).|| < r by A3;

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

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

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

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