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 ;
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 ;
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 ;
then ||.((seq . n) - (seq . m)).|| = ||.((yseq . n) - (yseq . m)).|| by ;
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 ;
rng yseq = rng seq ;
then reconsider lyseq = lim yseq as Point of X by ;
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 ;
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 ;
then ||.((yseq . n) - (lim yseq)).|| = ||.((seq . n) - lyseq).|| by ;
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