let V be RealNormSpace; :: thesis: for V1 being SubRealNormSpace of V
for CV1 being Subset of V st V1 is complete & CV1 = the carrier of V1 holds
CV1 is closed
let V1 be SubRealNormSpace of V; :: thesis: for CV1 being Subset of V st V1 is complete & CV1 = the carrier of V1 holds
CV1 is closed
let CV1 be Subset of V; :: thesis: ( V1 is complete & CV1 = the carrier of V1 implies CV1 is closed )
assume A1: ( V1 is complete & CV1 = the carrier of V1 ) ; :: thesis: CV1 is closed
for s1 being sequence of V st rng s1 c= CV1 & s1 is convergent holds
lim s1 in CV1

proof

let s1 be sequence of V; :: thesis: ( rng s1 c= CV1 & s1 is convergent implies lim s1 in CV1 )
assume A2: ( rng s1 c= CV1 & s1 is convergent ) ; :: thesis: lim s1 in CV1
then reconsider s2 = s1 as sequence of V1 by A1, FUNCT_2:6;
for s being Real st 0 < s holds
ex n being Nat st
for m being Nat st n <= m holds
||.((s2 . m) - (s2 . n)).|| < s

proof

let s be Real; :: thesis: ( 0 < s implies ex n being Nat st
for m being Nat st n <= m holds
||.((s2 . m) - (s2 . n)).|| < s )
assume 0 < s ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
||.((s2 . m) - (s2 . n)).|| < s
then consider n being Nat such that
A3: for m being Nat st n <= m holds
||.((s1 . m) - (s1 . n)).|| < s by A2, LOPBAN_3:4;
take n ; :: thesis: for m being Nat st n <= m holds
||.((s2 . m) - (s2 . n)).|| < s
let m be Nat; :: thesis: ( n <= m implies ||.((s2 . m) - (s2 . n)).|| < s )
assume n <= m ; :: thesis: ||.((s2 . m) - (s2 . n)).|| < s
then A4: ||.((s1 . m) - (s1 . n)).|| < s by A3;
- (s1 . n) = (- 1) * (s1 . n) by RLVECT_1:16
.= (- 1) * (s2 . n) by SUBTH0
.= - (s2 . n) by RLVECT_1:16 ;
then (s1 . m) - (s1 . n) = (s2 . m) - (s2 . n) by SUBTH0;
hence ||.((s2 . m) - (s2 . n)).|| < s by A4, SUBTH0; :: thesis: verum

end;

then A6: s2 is convergent by A1, LOPBAN_1:def 15, LOPBAN_3:5;
the carrier of V1 c= the carrier of V by DUALSP01:def 16;
then reconsider s0 = lim s2 as Point of V ;
for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((s1 . n) - s0).|| < r

proof

let r be Real; :: thesis: ( 0 < r implies ex m being Nat st
for n being Nat st m <= n holds
||.((s1 . n) - s0).|| < r )
assume 0 < r ; :: thesis: ex m being Nat st
for n being Nat st m <= n holds
||.((s1 . n) - s0).|| < r
then consider m being Nat such that
A7: for n being Nat st m <= n holds
||.((s2 . n) - (lim s2)).|| < r by A6, NORMSP_1:def 7;
take m ; :: thesis: for n being Nat st m <= n holds
||.((s1 . n) - s0).|| < r
let n be Nat; :: thesis: ( m <= n implies ||.((s1 . n) - s0).|| < r )
assume m <= n ; :: thesis: ||.((s1 . n) - s0).|| < r
then A8: ||.((s2 . n) - (lim s2)).|| < r by A7;
- (lim s2) = (- 1) * (lim s2) by RLVECT_1:16
.= (- 1) * s0 by SUBTH0
.= - s0 by RLVECT_1:16 ;
then (s2 . n) - (lim s2) = (s1 . n) - s0 by SUBTH0;
hence ||.((s1 . n) - s0).|| < r by A8, SUBTH0; :: thesis: verum

end;

then lim s1 = s0 by A2, NORMSP_1:def 7;
hence lim s1 in CV1 by A1; :: thesis: verum

end;

hence CV1 is closed ; :: thesis: verum