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

let e1 be real number ; :: thesis: ( e1 > 0 implies ex k being Element of NAT st
for m being Element of NAT st m >= k holds
abs ((||.seq.|| . m) - ||.(lim seq).||) < e1 )
assume A3: e1 > 0 ; :: thesis: ex k being Element of NAT st
for m being Element of NAT st m >= k holds
abs ((||.seq.|| . m) - ||.(lim seq).||) < e1
reconsider e = e1 as Real by XREAL_0:def 1;
consider k being Element of NAT such that
A4: for n being Element of NAT st n >= k holds
||.((seq . n) - (lim seq)).|| < e by A1, A3, CLVECT_1:def 18;
take k = k; :: thesis: for m being Element of NAT st m >= k holds
abs ((||.seq.|| . m) - ||.(lim seq).||) < e1

now

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

end;

hence for m being Element of NAT st m >= k holds
abs ((||.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