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

let seq be sequence of X; :: thesis: for g being Point of X st seq is convergent & lim seq = g holds
( ||.seq.|| is convergent & lim ||.seq.|| = )

let g be Point of X; :: thesis: ( seq is convergent & lim seq = g implies ( ||.seq.|| is convergent & lim ||.seq.|| = ) )
assume that
A1: seq is convergent and
A2: lim seq = g ; :: thesis: ( ||.seq.|| is convergent & lim ||.seq.|| = )
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) - ).| < r
let r be Real; :: thesis: ( r > 0 implies ex k being Nat st
for n being Nat st k <= n holds
|.((||.seq.|| . n) - ).| < r )

assume A4: r > 0 ; :: thesis: ex k being Nat st
for n being Nat st k <= n holds
|.((||.seq.|| . n) - ).| < r

consider m1 being Nat such that
A5: for n being Nat st n >= m1 holds
||.((seq . n) - g).|| < r by ;
take k = m1; :: thesis: for n being Nat st k <= n holds
|.((||.seq.|| . n) - ).| < r

now :: thesis: for n being Nat st n >= k holds
|.((||.seq.|| . n) - ).| < r
let n be Nat; :: thesis: ( n >= k implies |.((||.seq.|| . n) - ).| < r )
assume n >= k ; :: thesis: |.((||.seq.|| . n) - ).| < r
then A6: ||.((seq . n) - g).|| < r by A5;
|.(||.(seq . n).|| - ).| <= ||.((seq . n) - g).|| by CLVECT_1:110;
then |.(||.(seq . n).|| - ).| < r by ;
hence |.((||.seq.|| . n) - ).| < r by NORMSP_0:def 4; :: thesis: verum
end;
hence for n being Nat st k <= n holds
|.((||.seq.|| . n) - ).| < r ; :: thesis: verum
end;
||.seq.|| is convergent by ;
hence ( ||.seq.|| is convergent & lim ||.seq.|| = ) by ; :: thesis: verum