let X be RealNormSpace; :: thesis: for Y being Subset of X
for v being object holds
( v in Cl Y iff ex seq being sequence of X st
( rng seq c= Y & seq is convergent & lim seq = v ) )

let Y be Subset of X; :: thesis: for v being object holds
( v in Cl Y iff ex seq being sequence of X st
( rng seq c= Y & seq is convergent & lim seq = v ) )

let v be object ; :: thesis: ( v in Cl Y iff ex seq being sequence of X st
( rng seq c= Y & seq is convergent & lim seq = v ) )

reconsider Z = Y as Subset of by NORMSP_2:def 4;
A1: Cl Z = Cl Y by EQCL1;
hereby :: thesis: ( ex seq being sequence of X st
( rng seq c= Y & seq is convergent & lim seq = v ) implies v in Cl Y )
assume A2: v in Cl Y ; :: thesis: ex seq being Function of NAT,X st
( rng seq c= Y & seq is convergent & lim seq = v )

then A3: for G being Subset of st G is open & v in G holds
G meets Z by ;
reconsider v0 = v as Point of X by A2;
defpred S1[ Nat, Point of X] means ( ||.(v0 - \$2).|| < 1 / (\$1 + 1) & \$2 in Y );
A4: for n being Element of NAT ex w being Element of X st S1[n,w]
proof
let n be Element of NAT ; :: thesis: ex w being Element of X st S1[n,w]
set e = 1 / (n + 1);
for x being object st x in { y where y is Point of X : ||.(v0 - y).|| < 1 / (n + 1) } holds
x in the carrier of
proof
let x be object ; :: thesis: ( x in { y where y is Point of X : ||.(v0 - y).|| < 1 / (n + 1) } implies x in the carrier of )
assume x in { y where y is Point of X : ||.(v0 - y).|| < 1 / (n + 1) } ; :: thesis: x in the carrier of
then ex y being Point of X st
( x = y & ||.(v0 - y).|| < 1 / (n + 1) ) ;
then x in the carrier of X ;
hence x in the carrier of by NORMSP_2:def 4; :: thesis: verum
end;
then reconsider G = { y where y is Point of X : ||.(v0 - y).|| < 1 / (n + 1) } as Subset of by TARSKI:def 3;
||.(v0 - v0).|| < 1 / (n + 1) by NORMSP_1:6;
then v0 in G ;
then G meets Z by ;
then consider w being object such that
A5: w in G /\ Z by XBOOLE_0:def 1;
A6: ( w in G & w in Z ) by ;
then A7: ex y being Point of X st
( w = y & ||.(v0 - y).|| < 1 / (n + 1) ) ;
reconsider w = w as Point of X by A6;
take w ; :: thesis: S1[n,w]
thus S1[n,w] by A5, A7, XBOOLE_0:def 4; :: thesis: verum
end;
consider seq being Function of NAT,X such that
A8: for n being Element of NAT holds S1[n,seq . n] from take seq = seq; :: thesis: ( rng seq c= Y & seq is convergent & lim seq = v )
for y being object st y in rng seq holds
y in Y
proof
let y be object ; :: thesis: ( y in rng seq implies y in Y )
assume y in rng seq ; :: thesis: y in Y
then ex x being object st
( x in NAT & seq . x = y ) by FUNCT_2:11;
hence y in Y by A8; :: thesis: verum
end;
hence rng seq c= Y ; :: thesis: ( seq is convergent & lim seq = v )
A10: now :: thesis: for s being Real st 0 < s holds
ex k being Nat st
for m being Nat st k <= m holds
||.((seq . m) - v0).|| < s
let s be Real; :: thesis: ( 0 < s implies ex k being Nat st
for m being Nat st k <= m holds
||.((seq . m) - v0).|| < s )

consider n being Nat such that
A11: s " < n by SEQ_4:3;
assume A12: 0 < s ; :: thesis: ex k being Nat st
for m being Nat st k <= m holds
||.((seq . m) - v0).|| < s

(s ") + 0 < n + 1 by ;
then 1 / (n + 1) < 1 / (s ") by ;
then A13: 1 / (n + 1) < s by XCMPLX_1:216;
take k = n; :: thesis: for m being Nat st k <= m holds
||.((seq . m) - v0).|| < s

let m be Nat; :: thesis: ( k <= m implies ||.((seq . m) - v0).|| < s )
A14: m in NAT by ORDINAL1:def 12;
assume k <= m ; :: thesis: ||.((seq . m) - v0).|| < s
then k + 1 <= m + 1 by XREAL_1:6;
then 1 / (m + 1) <= 1 / (k + 1) by XREAL_1:118;
then 1 / (m + 1) < s by ;
then ||.(v0 - (seq . m)).|| < s by ;
hence ||.((seq . m) - v0).|| < s by NORMSP_1:7; :: thesis: verum
end;
hence seq is convergent ; :: thesis: lim seq = v
hence lim seq = v by ; :: thesis: verum
end;
given seq being sequence of X such that A15: rng seq c= Y and
A16: seq is convergent and
A17: lim seq = v ; :: thesis: v in Cl Y
v in the carrier of X by A17;
then A18: v in the carrier of by NORMSP_2:def 4;
reconsider v0 = v as Point of X by A17;
for G being Subset of st G is open & v in G holds
G meets Z
proof
let G be Subset of ; :: thesis: ( G is open & v in G implies G meets Z )
assume ( G is open & v in G ) ; :: thesis: G meets Z
then consider r being Real such that
A20: ( r > 0 & { y where y is Point of X : ||.(v0 - y).|| < r } c= G ) by NORMSP_2:22;
consider m being Nat such that
A21: for n being Nat st m <= n holds
||.((seq . n) - v0).|| < r by ;
||.((seq . m) - v0).|| < r by A21;
then ||.(v0 - (seq . m)).|| < r by NORMSP_1:7;
then A22: seq . m in { y where y is Point of X : ||.(v0 - y).|| < r } ;
seq . m in rng seq by ;
hence G meets Z by ; :: thesis: verum
end;
hence v in Cl Y by ; :: thesis: verum