theorem Th30: :: CC0SP2:30

for X being ComplexBanachSpace
for Y being Subset of X
for seq being sequence of X st Y is closed & rng seq c= Y & seq is CCauchy holds
( seq is convergent & lim seq in Y ) by CLOPBAN1:def 13, NCFCONT1:def 3;