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

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

hence
X is complete
; :: thesis: verumseq 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

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

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

then A5:
yseq 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

||.((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

||.((yseq . n) - (yseq . m)).|| < r ; :: thesis: verum

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

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

||.((yseq . n) - (yseq . m)).|| < r ; :: thesis: verum

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

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) - 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

||.((seq . n) - lyseq).|| < r ; :: thesis: verum

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

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

||.((seq . n) - lyseq).|| < r ; :: thesis: verum