thus for vseq being sequence of Complex_l1_Space st vseq is CCauchy holds
vseq is convergent by CSSPACE3:9; :: according to CLOPBAN1:def 13 :: thesis: verum