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 ;
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 ;
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 ; :: thesis: verum
end;
then A6: s2 is convergent by ;
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 ;
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 ; :: thesis: verum
end;
then lim s1 = s0 by ;
hence lim s1 in CV1 by A1; :: thesis: verum
end;
hence CV1 is closed ; :: thesis: verum