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 (LinearTopSpaceNorm X) by NORMSP_2:def 4;

A1: Cl Z = Cl Y by EQCL1;

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 (LinearTopSpaceNorm X) by NORMSP_2:def 4;

reconsider v0 = v as Point of X by A17;

for G being Subset of (LinearTopSpaceNorm X) st G is open & v in G holds

G meets Z

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 (LinearTopSpaceNorm X) 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 )

given seq being sequence of X such that A15:
rng seq c= Y
and ( 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 (LinearTopSpaceNorm X) st G is open & v in G holds

G meets Z by A1, PRE_TOPC:def 7;

reconsider v0 = v as Point of X by A2;

defpred S_{1}[ 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 S_{1}[n,w]

A8: for n being Element of NAT holds S_{1}[n,seq . n]
from FUNCT_2:sch 3(A4);

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

hence lim seq = v by A10, NORMSP_1:def 7; :: thesis: verum

end;( rng seq c= Y & seq is convergent & lim seq = v )

then A3: for G being Subset of (LinearTopSpaceNorm X) st G is open & v in G holds

G meets Z by A1, PRE_TOPC:def 7;

reconsider v0 = v as Point of X by A2;

defpred S

A4: for n being Element of NAT ex w being Element of X st S

proof

consider seq being Function of NAT,X such that
let n be Element of NAT ; :: thesis: ex w being Element of X st S_{1}[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 (LinearTopSpaceNorm X)

||.(v0 - v0).|| < 1 / (n + 1) by NORMSP_1:6;

then v0 in G ;

then G meets Z by A3, NORMSP_2:23;

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 A5, XBOOLE_0:def 4;

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: S_{1}[n,w]

thus S_{1}[n,w]
by A5, A7, XBOOLE_0:def 4; :: thesis: verum

end;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 (LinearTopSpaceNorm X)

proof

then reconsider G = { y where y is Point of X : ||.(v0 - y).|| < 1 / (n + 1) } as Subset of (LinearTopSpaceNorm X) by TARSKI:def 3;
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 (LinearTopSpaceNorm X) )

assume x in { y where y is Point of X : ||.(v0 - y).|| < 1 / (n + 1) } ; :: thesis: x in the carrier of (LinearTopSpaceNorm X)

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 (LinearTopSpaceNorm X) by NORMSP_2:def 4; :: thesis: verum

end;assume x in { y where y is Point of X : ||.(v0 - y).|| < 1 / (n + 1) } ; :: thesis: x in the carrier of (LinearTopSpaceNorm X)

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 (LinearTopSpaceNorm X) by NORMSP_2:def 4; :: thesis: verum

||.(v0 - v0).|| < 1 / (n + 1) by NORMSP_1:6;

then v0 in G ;

then G meets Z by A3, NORMSP_2:23;

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 A5, XBOOLE_0:def 4;

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: S

thus S

A8: for n being Element of NAT holds S

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

hence
rng seq c= Y
; :: thesis: ( seq is convergent & lim seq = v )
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;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

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

hence
seq is convergent
; :: thesis: lim seq = vex 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 A11, XREAL_1:8;

then 1 / (n + 1) < 1 / (s ") by A12, XREAL_1:76;

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 A13, XXREAL_0:2;

then ||.(v0 - (seq . m)).|| < s by A8, A14, XXREAL_0:2;

hence ||.((seq . m) - v0).|| < s by NORMSP_1:7; :: thesis: verum

end;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 A11, XREAL_1:8;

then 1 / (n + 1) < 1 / (s ") by A12, XREAL_1:76;

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 A13, XXREAL_0:2;

then ||.(v0 - (seq . m)).|| < s by A8, A14, XXREAL_0:2;

hence ||.((seq . m) - v0).|| < s by NORMSP_1:7; :: thesis: verum

hence lim seq = v by A10, NORMSP_1:def 7; :: thesis: verum

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 (LinearTopSpaceNorm X) by NORMSP_2:def 4;

reconsider v0 = v as Point of X by A17;

for G being Subset of (LinearTopSpaceNorm X) st G is open & v in G holds

G meets Z

proof

hence
v in Cl Y
by A1, A18, PRE_TOPC:def 7; :: thesis: verum
let G be Subset of (LinearTopSpaceNorm X); :: 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 A16, A17, A20, NORMSP_1:def 7;

||.((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 FUNCT_2:4, ORDINAL1:def 12;

hence G meets Z by A15, A20, A22, XBOOLE_0:def 4; :: thesis: verum

end;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 A16, A17, A20, NORMSP_1:def 7;

||.((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 FUNCT_2:4, ORDINAL1:def 12;

hence G meets Z by A15, A20, A22, XBOOLE_0:def 4; :: thesis: verum