let X be complete RealNormSpace; :: thesis: 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 )
let Y be Subset of X; :: thesis: 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 )
let seq be sequence of X; :: thesis: ( Y is closed & rng seq c= Y & seq is CCauchy implies ( seq is convergent & lim seq in Y ) )
assume AS: ( Y is closed & rng seq c= Y & seq is CCauchy ) ; :: thesis: ( seq is convergent & lim seq in Y )
hence seq is convergent by LOPBAN_1:def 16; :: thesis: lim seq in Y
hence lim seq in Y by AS, NFCONT_1:def 5; :: thesis: verum