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