let V be RealBanachSpace; :: thesis: for V1 being SubRealNormSpace of V st ex CV1 being Subset of V st

( CV1 = the carrier of V1 & CV1 is closed ) holds

V1 is RealBanachSpace

let V1 be SubRealNormSpace of V; :: thesis: ( ex CV1 being Subset of V st

( CV1 = the carrier of V1 & CV1 is closed ) implies V1 is RealBanachSpace )

given CV1 being Subset of V such that A1: ( CV1 = the carrier of V1 & CV1 is closed ) ; :: thesis: V1 is RealBanachSpace

for seq being sequence of V1 st seq is Cauchy_sequence_by_Norm holds

seq is convergent

( CV1 = the carrier of V1 & CV1 is closed ) holds

V1 is RealBanachSpace

let V1 be SubRealNormSpace of V; :: thesis: ( ex CV1 being Subset of V st

( CV1 = the carrier of V1 & CV1 is closed ) implies V1 is RealBanachSpace )

given CV1 being Subset of V such that A1: ( CV1 = the carrier of V1 & CV1 is closed ) ; :: thesis: V1 is RealBanachSpace

for seq being sequence of V1 st seq is Cauchy_sequence_by_Norm holds

seq is convergent

proof

hence
V1 is RealBanachSpace
by LOPBAN_1:def 15; :: thesis: verum
let seq be sequence of V1; :: thesis: ( seq is Cauchy_sequence_by_Norm implies seq is convergent )

assume A2: seq is Cauchy_sequence_by_Norm ; :: thesis: seq is convergent

the carrier of V1 c= the carrier of V by DUALSP01:def 16;

then reconsider seq1 = seq as sequence of V by FUNCT_2:7;

for r being Real st r > 0 holds

ex k being Nat st

for n, m being Nat st n >= k & m >= k holds

||.((seq1 . n) - (seq1 . m)).|| < r

rng seq c= CV1 by A1;

then reconsider s = lim seq1 as Point of V1 by A1, A6;

for r being Real st 0 < r holds

ex m being Nat st

for n being Nat st m <= n holds

||.((seq . n) - s).|| < r

end;assume A2: seq is Cauchy_sequence_by_Norm ; :: thesis: seq is convergent

the carrier of V1 c= the carrier of V by DUALSP01:def 16;

then reconsider seq1 = seq as sequence of V by FUNCT_2:7;

for r being Real st r > 0 holds

ex k being Nat st

for n, m being Nat st n >= k & m >= k holds

||.((seq1 . n) - (seq1 . m)).|| < r

proof

then A6:
seq1 is convergent
by LOPBAN_1:def 15, RSSPACE3:8;
let r be Real; :: thesis: ( r > 0 implies ex k being Nat st

for n, m being Nat st n >= k & m >= k holds

||.((seq1 . n) - (seq1 . m)).|| < r )

assume r > 0 ; :: thesis: ex k being Nat st

for n, m being Nat st n >= k & m >= k holds

||.((seq1 . n) - (seq1 . m)).|| < r

then consider k being Nat such that

A3: for n, m being Nat st n >= k & m >= k holds

||.((seq . n) - (seq . m)).|| < r by A2, RSSPACE3:8;

take k ; :: thesis: for n, m being Nat st n >= k & m >= k holds

||.((seq1 . n) - (seq1 . m)).|| < r

let n, m be Nat; :: thesis: ( n >= k & m >= k implies ||.((seq1 . n) - (seq1 . m)).|| < r )

assume ( n >= k & m >= k ) ; :: thesis: ||.((seq1 . n) - (seq1 . m)).|| < r

then A4: ||.((seq . n) - (seq . m)).|| < r by A3;

- (seq . m) = (- 1) * (seq . m) by RLVECT_1:16

.= (- 1) * (seq1 . m) by SUBTH0

.= - (seq1 . m) by RLVECT_1:16 ;

then (seq . n) - (seq . m) = (seq1 . n) - (seq1 . m) by SUBTH0;

hence ||.((seq1 . n) - (seq1 . m)).|| < r by A4, SUBTH0; :: thesis: verum

end;for n, m being Nat st n >= k & m >= k holds

||.((seq1 . n) - (seq1 . m)).|| < r )

assume r > 0 ; :: thesis: ex k being Nat st

for n, m being Nat st n >= k & m >= k holds

||.((seq1 . n) - (seq1 . m)).|| < r

then consider k being Nat such that

A3: for n, m being Nat st n >= k & m >= k holds

||.((seq . n) - (seq . m)).|| < r by A2, RSSPACE3:8;

take k ; :: thesis: for n, m being Nat st n >= k & m >= k holds

||.((seq1 . n) - (seq1 . m)).|| < r

let n, m be Nat; :: thesis: ( n >= k & m >= k implies ||.((seq1 . n) - (seq1 . m)).|| < r )

assume ( n >= k & m >= k ) ; :: thesis: ||.((seq1 . n) - (seq1 . m)).|| < r

then A4: ||.((seq . n) - (seq . m)).|| < r by A3;

- (seq . m) = (- 1) * (seq . m) by RLVECT_1:16

.= (- 1) * (seq1 . m) by SUBTH0

.= - (seq1 . m) by RLVECT_1:16 ;

then (seq . n) - (seq . m) = (seq1 . n) - (seq1 . m) by SUBTH0;

hence ||.((seq1 . n) - (seq1 . m)).|| < r by A4, SUBTH0; :: thesis: verum

rng seq c= CV1 by A1;

then reconsider s = lim seq1 as Point of V1 by A1, A6;

for r being Real st 0 < r holds

ex m being Nat st

for n being Nat st m <= n holds

||.((seq . n) - s).|| < r

proof

hence
seq is convergent
; :: thesis: verum
let r be Real; :: thesis: ( 0 < r implies ex m being Nat st

for n being Nat st m <= n holds

||.((seq . n) - s).|| < r )

assume r > 0 ; :: thesis: ex m being Nat st

for n being Nat st m <= n holds

||.((seq . n) - s).|| < r

then consider m being Nat such that

A7: for n being Nat st m <= n holds

||.((seq1 . n) - (lim seq1)).|| < r by A6, NORMSP_1:def 7;

take m ; :: thesis: for n being Nat st m <= n holds

||.((seq . n) - s).|| < r

let n be Nat; :: thesis: ( m <= n implies ||.((seq . n) - s).|| < r )

assume m <= n ; :: thesis: ||.((seq . n) - s).|| < r

then A8: ||.((seq1 . n) - (lim seq1)).|| < r by A7;

- (lim seq1) = (- 1) * (lim seq1) by RLVECT_1:16

.= (- 1) * s by SUBTH0

.= - s by RLVECT_1:16 ;

then (seq1 . n) - (lim seq1) = (seq . n) - s by SUBTH0;

hence ||.((seq . n) - s).|| < r by A8, SUBTH0; :: thesis: verum

end;for n being Nat st m <= n holds

||.((seq . n) - s).|| < r )

assume r > 0 ; :: thesis: ex m being Nat st

for n being Nat st m <= n holds

||.((seq . n) - s).|| < r

then consider m being Nat such that

A7: for n being Nat st m <= n holds

||.((seq1 . n) - (lim seq1)).|| < r by A6, NORMSP_1:def 7;

take m ; :: thesis: for n being Nat st m <= n holds

||.((seq . n) - s).|| < r

let n be Nat; :: thesis: ( m <= n implies ||.((seq . n) - s).|| < r )

assume m <= n ; :: thesis: ||.((seq . n) - s).|| < r

then A8: ||.((seq1 . n) - (lim seq1)).|| < r by A7;

- (lim seq1) = (- 1) * (lim seq1) by RLVECT_1:16

.= (- 1) * s by SUBTH0

.= - s by RLVECT_1:16 ;

then (seq1 . n) - (lim seq1) = (seq . n) - s by SUBTH0;

hence ||.((seq . n) - s).|| < r by A8, SUBTH0; :: thesis: verum