let X be RealNormSpace; :: thesis: for V being Subset of X

for Vt being Subset of (TopSpaceNorm X) st V = Vt holds

( V is closed iff Vt is closed )

let V be Subset of X; :: thesis: for Vt being Subset of (TopSpaceNorm X) st V = Vt holds

( V is closed iff Vt is closed )

let Vt be Subset of (TopSpaceNorm X); :: thesis: ( V = Vt implies ( V is closed iff Vt is closed ) )

assume A1: V = Vt ; :: thesis: ( V is closed iff Vt is closed )

for Vt being Subset of (TopSpaceNorm X) st V = Vt holds

( V is closed iff Vt is closed )

let V be Subset of X; :: thesis: for Vt being Subset of (TopSpaceNorm X) st V = Vt holds

( V is closed iff Vt is closed )

let Vt be Subset of (TopSpaceNorm X); :: thesis: ( V = Vt implies ( V is closed iff Vt is closed ) )

assume A1: V = Vt ; :: thesis: ( V is closed iff Vt is closed )

hereby :: thesis: ( Vt is closed implies V is closed )

assume A5:
Vt is closed
; :: thesis: V is closed assume A2:
V is closed
; :: thesis: Vt is closed

end;now :: thesis: for St being sequence of (TopSpaceNorm X) st St is convergent & rng St c= Vt holds

Lim St c= Vt

hence
Vt is closed
by FRECHET:def 7; :: thesis: verumLim St c= Vt

let St be sequence of (TopSpaceNorm X); :: thesis: ( St is convergent & rng St c= Vt implies Lim St c= Vt )

assume that

A3: St is convergent and

A4: rng St c= Vt ; :: thesis: Lim St c= Vt

reconsider S = St as sequence of X ;

S is convergent by A3, Th13;

then lim S in V by A1, A2, A4, NFCONT_1:def 3;

then {(lim S)} c= V by ZFMISC_1:31;

hence Lim St c= Vt by A1, A3, Th14; :: thesis: verum

end;assume that

A3: St is convergent and

A4: rng St c= Vt ; :: thesis: Lim St c= Vt

reconsider S = St as sequence of X ;

S is convergent by A3, Th13;

then lim S in V by A1, A2, A4, NFCONT_1:def 3;

then {(lim S)} c= V by ZFMISC_1:31;

hence Lim St c= Vt by A1, A3, Th14; :: thesis: verum

now :: thesis: for S being sequence of X st rng S c= V & S is convergent holds

lim S in V

hence
V is closed
by NFCONT_1:def 3; :: thesis: verumlim S in V

let S be sequence of X; :: thesis: ( rng S c= V & S is convergent implies lim S in V )

assume that

A6: rng S c= V and

A7: S is convergent ; :: thesis: lim S in V

reconsider St = S as sequence of (TopSpaceNorm X) ;

A8: St is convergent by A7, Th13;

then Lim St c= Vt by A1, A5, A6, FRECHET:def 7;

then {(lim S)} c= V by A1, A8, Th14;

hence lim S in V by ZFMISC_1:31; :: thesis: verum

end;assume that

A6: rng S c= V and

A7: S is convergent ; :: thesis: lim S in V

reconsider St = S as sequence of (TopSpaceNorm X) ;

A8: St is convergent by A7, Th13;

then Lim St c= Vt by A1, A5, A6, FRECHET:def 7;

then {(lim S)} c= V by A1, A8, Th14;

hence lim S in V by ZFMISC_1:31; :: thesis: verum