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: ||.(S - g).|| is convergent by A1, Th117, Th119;

now

let r be real number ; :: thesis: ( 0 < r implies ex k being Element of NAT st
for n being Element of NAT st k <= n holds
abs ((||.(S - g).|| . n) - 0 ) < r )
A4: r is Real by XREAL_0:def 1;
assume 0 < r ; :: thesis: ex k being Element of NAT st
for n being Element of NAT st k <= n holds
abs ((||.(S - g).|| . n) - 0 ) < r
then consider m1 being Element of NAT such that
A5: for n being Element of NAT st m1 <= n holds
||.((S . n) - g).|| < r by A1, A2, A4, Def18;
take k = m1; :: thesis: for n being Element of NAT st k <= n holds
abs ((||.(S - g).|| . n) - 0 ) < r
let n be Element of NAT ; :: thesis: ( k <= n implies abs ((||.(S - g).|| . n) - 0 ) < r )
assume k <= n ; :: thesis: abs ((||.(S - g).|| . n) - 0 ) < r
then ||.((S . n) - g).|| < r by A5;
then A6: ||.(((S . n) - g) - H₁(CNS)).|| < r by RLVECT_1:26;
abs (||.((S . n) - g).|| - ||.H₁(CNS).||) <= ||.(((S . n) - g) - H₁(CNS)).|| by Th111;
then abs (||.((S . n) - g).|| - ||.H₁(CNS).||) < r by A6, XXREAL_0:2;
then abs (||.((S . n) - g).|| - 0 ) < r by Def11;
then abs (||.((S - g) . n).|| - 0 ) < r by NORMSP_1:def 7;
hence abs ((||.(S - g).|| . n) - 0 ) < r by Def17; :: thesis: verum

end;

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