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;

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

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

now :: thesis: for n being Nat st n >= k 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;

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

end;

hence ||.seq.|| is convergent by SEQ_2:def 6; :: thesis: verum