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

proof

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

proof

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;

then A6: seq1 is convergent by LOPBAN_1:def 15, RSSPACE3:8;
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

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;

hence seq is convergent ; :: thesis: verum

end;

hence V1 is RealBanachSpace by LOPBAN_1:def 15; :: thesis: verum