let X be RealBanachSpace; :: 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 A1: ( 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 15; :: thesis: lim seq in Y
hence lim seq in Y by A1, NFCONT_1:def 3; :: thesis: verum