theorem :: CSSPACE3:9

for vseq being sequence of Complex_l1_Space st vseq is Cauchy_sequence_by_Norm holds
vseq is convergent