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).|| )

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

( ||.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

then
||.seq.|| is convergent
by SEQ_2:def 6;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

|.((||.seq.|| . m) - ||.(lim seq).||).| < e1 ; :: thesis: verum

end;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

hence
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;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

|.((||.seq.|| . m) - ||.(lim seq).||).| < e1 ; :: thesis: verum

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