let Z be RealNormSpace; :: thesis: ( Z is complete iff MetricSpaceNorm Z is complete )
set N = MetricSpaceNorm Z;

hereby :: thesis: ( MetricSpaceNorm Z is complete implies Z is complete )

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

proof

let S2 be sequence of (MetricSpaceNorm Z); :: thesis: ( S2 is Cauchy implies S2 is convergent )
assume A2: S2 is Cauchy ; :: thesis: S2 is convergent
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: ( r > 0 implies ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((seq2 . n) - (seq2 . m)).|| < r )
assume r > 0 ; :: thesis: ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((seq2 . n) - (seq2 . m)).|| < r
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: for n, m being Nat st n >= p & m >= p holds
||.((seq2 . n) - (seq2 . m)).|| < r
let n, m be Nat; :: thesis: ( n >= p & m >= p implies ||.((seq2 . n) - (seq2 . m)).|| < r )
assume ( p <= n & p <= m ) ; :: thesis: ||.((seq2 . n) - (seq2 . m)).|| < r
then dist ((S2 . n),(S2 . m)) < r by A3;
hence ||.((seq2 . n) - (seq2 . m)).|| < r by NORMSP_2:def 1; :: thesis: verum

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: verum

end;

hence MetricSpaceNorm Z is complete ; :: thesis: verum

end;

assume A5: MetricSpaceNorm Z is complete ; :: thesis: Z is complete
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: ( seq2 is Cauchy_sequence_by_Norm implies seq2 is convergent )
assume A6: seq2 is Cauchy_sequence_by_Norm ; :: thesis: seq2 is convergent
reconsider S2 = seq2 as sequence of (MetricSpaceNorm Z) ;

now :: thesis: for r being Real st r > 0 holds
ex p being Nat st
for n, m being Nat st p <= n & p <= m holds
dist ((S2 . n),(S2 . m)) < r

let r be Real; :: thesis: ( r > 0 implies ex p being Nat st
for n, m being Nat st p <= n & p <= m holds
dist ((S2 . n),(S2 . m)) < r )
assume r > 0 ; :: thesis: ex p being Nat st
for n, m being Nat st p <= n & p <= m holds
dist ((S2 . n),(S2 . m)) < r
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: for n, m being Nat st p <= n & p <= m holds
dist ((S2 . n),(S2 . m)) < r
let n, m be Nat; :: thesis: ( p <= n & p <= m implies dist ((S2 . n),(S2 . m)) < r )
assume ( p <= n & p <= m ) ; :: thesis: dist ((S2 . n),(S2 . m)) < r
then ||.((seq2 . n) - (seq2 . m)).|| < r by A7;
hence dist ((S2 . n),(S2 . m)) < r by NORMSP_2:def 1; :: thesis: verum

end;

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

end;

hence Z is complete ; :: thesis: verum