now :: thesis:

let S1 be sequence of (MetricSpaceNorm X); :: thesis:
reconsider S2 = S1 as sequence of X ;
assume A1: S1 is Cauchy ; :: thesis:
S2 is Cauchy_sequence_by_Norm

proof

let r be Real; :: according to RSSPACE3:def 5 :: thesis:
assume r > 0 ; :: thesis:
then consider p being Nat such that
A2: for n, m being Nat st p <= n & p <= m holds
dist ((S1 . n),(S1 . m)) < r by A1, TBSP_1:def 4;

now :: thesis:

let n, m be Nat; :: thesis:
assume ( p <= n & p <= m ) ; :: thesis:
then dist ((S1 . n),(S1 . m)) < r by A2;
hence dist ((S2 . n),(S2 . m)) < r by NORMSP_2:def 1; :: thesis:

end;

hence ex b₁ being set st
for b₂, b₃ being set holds
( not b₁ <= b₂ or not b₁ <= b₃ or not r <= dist ((S2 . b₂),(S2 . b₃)) ) ; :: thesis:

end;

then S2 is convergent by LOPBAN_1:def 15;
hence S1 is convergent by NORMSP_2:5; :: thesis:

end;

hence MetricSpaceNorm X is complete by TBSP_1:def 5; :: thesis: