let CNS be ComplexNormSpace; :: thesis: for S being sequence of CNS st S is convergent holds
||.S.|| is convergent
let S be sequence of CNS; :: thesis: ( S is convergent implies ||.S.|| is convergent )
assume S is convergent ; :: thesis: ||.S.|| is convergent
then consider g being Point of CNS such that
A1: for r being Real st 0 < r holds
ex m being Element of NAT st
for n being Element of NAT st m <= n holds
||.((S . n) - g).|| < r by Def16;

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.|| . n) - ||.g.||) < r )
assume A2: 0 < r ; :: thesis: ex k being Element of NAT st
for n being Element of NAT st k <= n holds
abs ((||.S.|| . n) - ||.g.||) < r
r is Real by XREAL_0:def 1;
then consider m1 being Element of NAT such that
A3: for n being Element of NAT st m1 <= n holds
||.((S . n) - g).|| < r by A1, A2;
take k = m1; :: thesis: for n being Element of NAT st k <= n holds
abs ((||.S.|| . n) - ||.g.||) < r
let n be Element of NAT ; :: thesis: ( k <= n implies abs ((||.S.|| . n) - ||.g.||) < r )
assume k <= n ; :: thesis: abs ((||.S.|| . n) - ||.g.||) < r
then A4: ||.((S . n) - g).|| < r by A3;
abs (||.(S . n).|| - ||.g.||) <= ||.((S . n) - g).|| by Th111;
then abs (||.(S . n).|| - ||.g.||) < r by A4, XXREAL_0:2;
hence abs ((||.S.|| . n) - ||.g.||) < r by NORMSP_0:def 4; :: thesis: verum

end;

hence ||.S.|| is convergent by SEQ_2:def 6; :: thesis: verum