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

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

assume x in Cl X ; :: thesis: ex S being sequence of M st
( ( for n being Nat holds S . n in X ) & S is convergent & lim S = x )
then consider St being sequence of (MetricSpaceNorm (RUSp2RNSp M)) such that
A1: for n being Nat holds St . n in X and
A2: ( St is convergent & lim St = x ) by TOPMETR4:5;
reconsider S = St as sequence of M ;
take S = S; :: thesis: ( ( for n being Nat holds S . n in X ) & S is convergent & lim S = x )
thus for n being Nat holds S . n in X by A1; :: thesis: ( S is convergent & lim S = x )
thus S is convergent by A2, Th5; :: thesis: lim S = x
thus lim S = x by Th6, A2; :: thesis: verum

end;

assume ex S being sequence of M st
( ( for n being Nat holds S . n in X ) & S is convergent & lim S = x ) ; :: thesis: x in Cl X
then consider S being sequence of M such that
A3: ( ( for n being Nat holds S . n in X ) & S is convergent & lim S = x ) ;
reconsider St = S as sequence of (MetricSpaceNorm (RUSp2RNSp M)) ;
A5: St is convergent by A3, Th5;
then lim St = x by A3, Th6;
hence x in Cl X by TOPMETR4:5, A3, A5; :: thesis: verum