now :: thesis: for S1 being sequence of (MetricSpaceNorm X) st S1 is Cauchy holds
S1 is convergent

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 Cauchy_sequence_by_Norm

proof

let r be Real; :: according to RSSPACE3:def 5 :: thesis: ( r <= 0 or 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₃)) ) )
assume r > 0 ; :: thesis: 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₃)) )
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: 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 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 set st
for b₂, b₃ being set 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 15;
hence S1 is convergent by NORMSP_2:5; :: thesis: verum

end;

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