let X be ComplexNormSpace; :: thesis: for seq being sequence of X st seq is convergent holds
( ||.seq.|| is convergent & lim ||.seq.|| = ||.(lim seq).|| )
let seq be sequence of X; :: thesis: ( seq is convergent implies ( ||.seq.|| is convergent & lim ||.seq.|| = ||.(lim seq).|| ) )
assume A1: seq is convergent ; :: thesis: ( ||.seq.|| is convergent & lim ||.seq.|| = ||.(lim seq).|| )

A2: now :: thesis: for e1 being Real st e1 > 0 holds
ex k being Nat st
for m being Nat st m >= k holds
|.((||.seq.|| . m) - ||.(lim seq).||).| < e1

let e1 be Real; :: thesis: ( e1 > 0 implies ex k being Nat st
for m being Nat st m >= k holds
|.((||.seq.|| . m) - ||.(lim seq).||).| < e1 )
assume A3: e1 > 0 ; :: thesis: ex k being Nat st
for m being Nat st m >= k holds
|.((||.seq.|| . m) - ||.(lim seq).||).| < e1
reconsider e = e1 as Real ;
consider k being Nat such that
A4: for n being Nat st n >= k holds
||.((seq . n) - (lim seq)).|| < e by A1, A3, CLVECT_1:def 16;
take k = k; :: thesis: for m being Nat st m >= k holds
|.((||.seq.|| . m) - ||.(lim seq).||).| < e1

now :: thesis: for m being Nat st m >= k holds
|.((||.seq.|| . m) - ||.(lim seq).||).| < e1

let m be Nat; :: thesis: ( m >= k implies |.((||.seq.|| . m) - ||.(lim seq).||).| < e1 )
assume m >= k ; :: thesis: |.((||.seq.|| . m) - ||.(lim seq).||).| < e1
then A5: ||.((seq . m) - (lim seq)).|| < e by A4;
||.(seq . m).|| = ||.seq.|| . m by NORMSP_0:def 4;
then |.((||.seq.|| . m) - ||.(lim seq).||).| <= ||.((seq . m) - (lim seq)).|| by CLVECT_1:110;
hence |.((||.seq.|| . m) - ||.(lim seq).||).| < e1 by A5, XXREAL_0:2; :: thesis: verum

end;

hence for m being Nat st m >= k holds
|.((||.seq.|| . m) - ||.(lim seq).||).| < e1 ; :: thesis: verum

end;

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