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

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

hence
CV1 is closed
; :: thesis: verum
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

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

hence lim s1 in CV1 by A1; :: thesis: verum

end;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

then A6:
s2 is convergent
by A1, LOPBAN_1:def 15, LOPBAN_3:5;
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;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

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

then
lim s1 = s0
by A2, NORMSP_1:def 7;
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;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

hence lim s1 in CV1 by A1; :: thesis: verum