let X be RealNormSpace; :: thesis: for Y being RealBanachSpace
for X0 being Subset of Y st X is Subspace of Y & the carrier of X = X0 & the normF of X = the normF of Y | the carrier of X & X0 is closed holds
X is complete
let Y be RealBanachSpace; :: thesis: for X0 being Subset of Y st X is Subspace of Y & the carrier of X = X0 & the normF of X = the normF of Y | the carrier of X & X0 is closed holds
X is complete
let X0 be Subset of Y; :: thesis: ( X is Subspace of Y & the carrier of X = X0 & the normF of X = the normF of Y | the carrier of X & X0 is closed implies X is complete )
assume A1: ( X is Subspace of Y & the carrier of X = X0 & the normF of X = the normF of Y | the carrier of X & X0 is closed ) ; :: thesis: X is complete

now :: thesis: for seq being sequence of X st seq is Cauchy_sequence_by_Norm holds
seq is convergent

let seq be sequence of X; :: thesis: ( seq is Cauchy_sequence_by_Norm implies seq is convergent )
assume A2: seq is Cauchy_sequence_by_Norm ; :: thesis: seq is convergent
rng seq c= the carrier of Y by A1, XBOOLE_1:1;
then reconsider yseq = seq as sequence of Y by FUNCT_2:6;
for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((yseq . n) - (yseq . 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
||.((yseq . n) - (yseq . m)).|| < r )
assume r > 0 ; :: thesis: ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((yseq . n) - (yseq . 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 RSSPACE3:8, A2;
take k ; :: thesis: for n, m being Nat st n >= k & m >= k holds
||.((yseq . n) - (yseq . m)).|| < r

now :: thesis: for n, m being Nat st n >= k & m >= k holds
||.((yseq . n) - (yseq . m)).|| < r

let n, m be Nat; :: thesis: ( n >= k & m >= k implies ||.((yseq . n) - (yseq . m)).|| < r )
assume A4: ( n >= k & m >= k ) ; :: thesis: ||.((yseq . n) - (yseq . m)).|| < r
(seq . n) - (seq . m) = (yseq . n) - (yseq . m) by A1, RLSUB_1:16;
then ||.((seq . n) - (seq . m)).|| = ||.((yseq . n) - (yseq . m)).|| by FUNCT_1:49, A1;
hence ||.((yseq . n) - (yseq . m)).|| < r by A4, A3; :: thesis: verum

end;

hence for n, m being Nat st n >= k & m >= k holds
||.((yseq . n) - (yseq . m)).|| < r ; :: thesis: verum

end;

then A5: yseq is convergent by LOPBAN_1:def 15, RSSPACE3:8;
rng yseq = rng seq ;
then reconsider lyseq = lim yseq as Point of X by A1, A5, NFCONT_1:def 3;
for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((seq . n) - lyseq).|| < 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) - lyseq).|| < r )
assume 0 < r ; :: thesis: ex m being Nat st
for n being Nat st m <= n holds
||.((seq . n) - lyseq).|| < r
then consider m being Nat such that
A6: for n being Nat st m <= n holds
||.((yseq . n) - (lim yseq)).|| < r by A5, NORMSP_1:def 7;
take m ; :: thesis: for n being Nat st m <= n holds
||.((seq . n) - lyseq).|| < r

now :: thesis: for n being Nat st m <= n holds
||.((seq . n) - lyseq).|| < r

let n be Nat; :: thesis: ( m <= n implies ||.((seq . n) - lyseq).|| < r )
assume A7: m <= n ; :: thesis: ||.((seq . n) - lyseq).|| < r
(yseq . n) - (lim yseq) = (seq . n) - lyseq by A1, RLSUB_1:16;
then ||.((yseq . n) - (lim yseq)).|| = ||.((seq . n) - lyseq).|| by FUNCT_1:49, A1;
hence ||.((seq . n) - lyseq).|| < r by A7, A6; :: thesis: verum

end;

hence for n being Nat st m <= n holds
||.((seq . n) - lyseq).|| < r ; :: thesis: verum

end;

hence seq is convergent ; :: thesis: verum

end;

hence X is complete ; :: thesis: verum