let Z be RealNormSpace; :: thesis:
set N = MetricSpaceNorm Z;

hereby :: thesis:

assume A1: Z is complete ; :: thesis:
for S2 being sequence of (MetricSpaceNorm Z) st S2 is Cauchy holds
S2 is convergent

proof

let S2 be sequence of (MetricSpaceNorm Z); :: thesis:
assume A2: S2 is Cauchy ; :: thesis:
reconsider seq2 = S2 as sequence of Z ;
for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((seq2 . n) - (seq2 . m)).|| < r

proof

let r be Real; :: thesis:
assume r > 0 ; :: thesis:
then consider p being Nat such that
A3: for n, m being Nat st p <= n & p <= m holds
dist ((S2 . n),(S2 . m)) < r by A2;
take p ; :: thesis:
let n, m be Nat; :: thesis:
assume ( p <= n & p <= m ) ; :: thesis:
then dist ((S2 . n),(S2 . m)) < r by A3;
hence ||.((seq2 . n) - (seq2 . m)).|| < r by NORMSP_2:def 1; :: thesis:

end;

then A4: seq2 is convergent by A1, RSSPACE3:8;
reconsider L = lim seq2 as Point of (MetricSpaceNorm Z) ;
for r being Real st 0 < r holds
ex m being Nat st
for n being Nat st m <= n holds
||.((seq2 . n) - (lim seq2)).|| < r by A4, NORMSP_1:def 7;
then S2 is_convergent_in_metrspace_to L by NORMSP_2:4;
hence S2 is convergent by METRIC_6:9; :: thesis:

end;

hence MetricSpaceNorm Z is complete ; :: thesis:

end;

assume A5: MetricSpaceNorm Z is complete ; :: thesis:
for seq2 being sequence of Z st seq2 is Cauchy_sequence_by_Norm holds
seq2 is convergent

proof

let seq2 be sequence of Z; :: thesis:
assume A6: seq2 is Cauchy_sequence_by_Norm ; :: thesis:
reconsider S2 = seq2 as sequence of (MetricSpaceNorm Z) ;

now :: thesis:

let r be Real; :: thesis:
assume r > 0 ; :: thesis:
then consider p being Nat such that
A7: for n, m being Nat st p <= n & p <= m holds
||.((seq2 . n) - (seq2 . m)).|| < r by A6, RSSPACE3:8;
take p = p; :: thesis:
let n, m be Nat; :: thesis:
assume ( p <= n & p <= m ) ; :: thesis:
then ||.((seq2 . n) - (seq2 . m)).|| < r by A7;
hence dist ((S2 . n),(S2 . m)) < r by NORMSP_2:def 1; :: thesis:

end;

then S2 is Cauchy ;
then S2 is convergent by A5;
hence seq2 is convergent by NORMSP_2:5; :: thesis:

end;

hence Z is complete ; :: thesis: