let M be RealUnitarySpace; :: thesis: for X being Subset of (TopSpaceNorm (RUSp2RNSp M)) holds
( X is closed iff for S being sequence of M st ( for n being Nat holds S . n in X ) & S is convergent holds
lim S in X )
let X be Subset of (TopSpaceNorm (RUSp2RNSp M)); :: thesis: ( X is closed iff for S being sequence of M st ( for n being Nat holds S . n in X ) & S is convergent holds
lim S in X )

hereby :: thesis: ( ( for S being sequence of M st ( for n being Nat holds S . n in X ) & S is convergent holds
lim S in X ) implies X is closed )

assume A1p: X is closed ; :: thesis: for S being sequence of M st ( for n being Nat holds S . n in X ) & S is convergent holds
lim S in X
thus for S being sequence of M st ( for n being Nat holds S . n in X ) & S is convergent holds
lim S in X :: thesis: verum

proof

let S be sequence of M; :: thesis: ( ( for n being Nat holds S . n in X ) & S is convergent implies lim S in X )
assume that
A2: for n being Nat holds S . n in X and
A3: S is convergent ; :: thesis: lim S in X
reconsider St = S as sequence of (MetricSpaceNorm (RUSp2RNSp M)) ;
A5: St is convergent by A3, Th5;
then lim St = lim S by Th6;
hence lim S in X by A2, A5, A1p, TOPMETR4:6; :: thesis: verum

end;

end;

assume A6: for S being sequence of M st ( for n being Nat holds S . n in X ) & S is convergent holds
lim S in X ; :: thesis: X is closed
for St being sequence of (MetricSpaceNorm (RUSp2RNSp M)) st ( for n being Nat holds St . n in X ) & St is convergent holds
lim St in X

proof

let St be sequence of (MetricSpaceNorm (RUSp2RNSp M)); :: thesis: ( ( for n being Nat holds St . n in X ) & St is convergent implies lim St in X )
assume that
A7: for n being Nat holds St . n in X and
A8: St is convergent ; :: thesis: lim St in X
reconsider S = St as sequence of M ;
A9: for n being Nat holds S . n in X by A7;
A10: S is convergent by A8, Th5;
lim St = lim S by A8, Th6;
hence lim St in X by A6, A9, A10; :: thesis: verum

end;

hence X is closed by TOPMETR4:6; :: thesis: verum