let X be NormedLinearTopSpace; :: thesis: for V being Subset of X holds
( V is closed iff for s1 being sequence of X st rng s1 c= V & s1 is convergent holds
lim s1 in V )
let V be Subset of X; :: thesis: ( V is closed iff for s1 being sequence of X st rng s1 c= V & s1 is convergent holds
lim s1 in V )
consider RNS being RealNormSpace such that
A1: ( RNS = NORMSTR(# the carrier of X, the ZeroF of X, the addF of X, the Mult of X, the normF of X #) & the topology of X = the topology of (TopSpaceNorm RNS) ) by Def7;
reconsider V0 = V as Subset of (TopSpaceNorm RNS) by A1;
reconsider V1 = V as Subset of RNS by A1;

hereby :: thesis: ( ( for s1 being sequence of X st rng s1 c= V & s1 is convergent holds
lim s1 in V ) implies V is closed )

assume V is closed ; :: thesis: for s1 being sequence of X st rng s1 c= V & s1 is convergent holds
lim s1 in V
then ([#] X) \ V is open ;
then ([#] (TopSpaceNorm RNS)) \ V0 is open by A1;
then V0 is closed ;
then A2: V1 is closed by NORMSP_2:15;
thus for s1 being sequence of X st rng s1 c= V & s1 is convergent holds
lim s1 in V :: thesis: verum

proof

let s1 be sequence of X; :: thesis: ( rng s1 c= V & s1 is convergent implies lim s1 in V )
assume A3: ( rng s1 c= V & s1 is convergent ) ; :: thesis: lim s1 in V
reconsider s2 = s1 as sequence of RNS by A1;
( s2 is convergent & lim s1 = lim s2 ) by A1, A3, Th26;
hence lim s1 in V by A2, A3; :: thesis: verum

end;

end;

assume A4: for s1 being sequence of X st rng s1 c= V & s1 is convergent holds
lim s1 in V ; :: thesis: V is closed
for s1 being sequence of RNS st rng s1 c= V1 & s1 is convergent holds
lim s1 in V1

proof

let s2 be sequence of RNS; :: thesis: ( rng s2 c= V1 & s2 is convergent implies lim s2 in V1 )
assume A5: ( rng s2 c= V1 & s2 is convergent ) ; :: thesis: lim s2 in V1
reconsider s1 = s2 as sequence of X by A1;
A6: s1 is convergent by A5, A1, Th27;
then lim s1 = lim s2 by A1, Th26;
hence lim s2 in V1 by A4, A6, A5; :: thesis: verum

end;

then V1 is closed ;
then V0 is closed by NORMSP_2:15;
then ([#] (TopSpaceNorm RNS)) \ V0 is open ;
then ([#] X) \ V is open by A1;
hence V is closed ; :: thesis: verum