now

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

proof

let r be Real; :: according to RSSPACE3:def 5 :: thesis: ( r <= 0 or ex b₁ being Element of NAT st
for b₂, b₃ being Element of NAT holds
( not b₁ <= b₂ or not b₁ <= b₃ or not r <= dist (S2 . b₂),(S2 . b₃) ) )
assume r > 0 ; :: thesis: ex b₁ being Element of NAT st
for b₂, b₃ being Element of NAT holds
( not b₁ <= b₂ or not b₁ <= b₃ or not r <= dist (S2 . b₂),(S2 . b₃) )
then consider p being Element of NAT such that
A2: for n, m being Element of NAT st p <= n & p <= m holds
dist (S1 . n),(S1 . m) < r by A1, TBSP_1:def 5;

now

let n, m be Element of 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 dist (S1 . n),(S1 . m) < r by A2;
hence dist (S2 . n),(S2 . m) < r by NORMSP_2:def 1; :: thesis: verum

end;

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

end;

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

end;

hence MetricSpaceNorm X is complete by TBSP_1:def 6; :: thesis: verum