let X be ComplexUnitarySpace; :: 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.|| )

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

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;
take k = m1; :: 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 A6: ||.((seq . n) - g).|| < r by A5;
|.(||.(seq . n).|| - ||.g.||).| <= ||.((seq . n) - g).|| by CSSPACE:49;
then |.(||.(seq . n).|| - ||.g.||).| < r by A6, 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;

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