theorem Th20: :: C0SP2:20

for X being RealBanachSpace
for Y being Subset of X
for seq being sequence of X st Y is closed & rng seq c= Y & seq is Cauchy_sequence_by_Norm holds
( seq is convergent & lim seq in Y ) by LOPBAN_1:def 15, NFCONT_1:def 3;