theorem :: RSSPACE3:9

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