thus for vseq being sequence of l1_Space st vseq is CCauchy holds
vseq is convergent by RSSPACE3:11; :: according to LOPBAN_1:def 16 :: thesis: verum