let CNS be ComplexNormSpace; :: thesis: for g being Point of CNS
for S being sequence of CNS st S is convergent & lim S = g holds
( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 )
let g be Point of CNS; :: thesis: for S being sequence of CNS st S is convergent & lim S = g holds
( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 )
let S be sequence of CNS; :: thesis: ( S is convergent & lim S = g implies ( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 ) )
assume that
A1: S is convergent and
A2: lim S = g ; :: thesis: ( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 )

A3: now :: thesis: for r being Real st 0 < r holds
ex k being Nat st
for n being Nat st k <= n holds
|.((||.(S - g).|| . n) - 0).| < r

let r be Real; :: thesis: ( 0 < r implies ex k being Nat st
for n being Nat st k <= n holds
|.((||.(S - g).|| . n) - 0).| < r )
assume A4: 0 < r ; :: thesis: ex k being Nat st
for n being Nat st k <= n holds
|.((||.(S - g).|| . n) - 0).| < r
consider m1 being Nat such that
A5: for n being Nat st m1 <= n holds
||.((S . n) - g).|| < r by A1, A2, A4, Def16;
take k = m1; :: thesis: for n being Nat st k <= n holds
|.((||.(S - g).|| . n) - 0).| < r
let n be Nat; :: thesis: ( k <= n implies |.((||.(S - g).|| . n) - 0).| < r )
assume k <= n ; :: thesis: |.((||.(S - g).|| . n) - 0).| < r
then ||.((S . n) - g).|| < r by A5;
then A6: ||.(((S . n) - g) - H₁(CNS)).|| < r by RLVECT_1:13;
|.(||.((S . n) - g).|| - ||.H₁(CNS).||).| <= ||.(((S . n) - g) - H₁(CNS)).|| by Th110;
then |.(||.((S . n) - g).|| - ||.H₁(CNS).||).| < r by A6, XXREAL_0:2;
then |.(||.((S . n) - g).|| - 0).| < r ;
then |.(||.((S - g) . n).|| - 0).| < r by NORMSP_1:def 4;
hence |.((||.(S - g).|| . n) - 0).| < r by NORMSP_0:def 4; :: thesis: verum

end;

||.(S - g).|| is convergent by A1, Th115, Th117;
hence ( ||.(S - g).|| is convergent & lim ||.(S - g).|| = 0 ) by A3, SEQ_2:def 7; :: thesis: verum