let n be Nat; :: thesis: for seq1 being sequence of ()
for seq2 being sequence of () st seq1 = seq2 & seq2 is Cauchy holds
seq1 is Cauchy_sequence_by_Norm

let seq1 be sequence of (); :: thesis: for seq2 being sequence of () st seq1 = seq2 & seq2 is Cauchy holds
seq1 is Cauchy_sequence_by_Norm

let seq2 be sequence of (); :: thesis: ( seq1 = seq2 & seq2 is Cauchy implies seq1 is Cauchy_sequence_by_Norm )
assume that
A1: seq1 = seq2 and
A2: seq2 is Cauchy ; :: thesis: seq1 is Cauchy_sequence_by_Norm
let r be Real; :: according to RSSPACE3:def 5 :: thesis: ( r <= 0 or ex b1 being set st
for b2, b3 being set holds
( not b1 <= b2 or not b1 <= b3 or not r <= dist ((seq1 . b2),(seq1 . b3)) ) )

assume r > 0 ; :: thesis: ex b1 being set st
for b2, b3 being set holds
( not b1 <= b2 or not b1 <= b3 or not r <= dist ((seq1 . b2),(seq1 . b3)) )

then consider k being Nat such that
A3: for m1, m2 being Nat st m1 >= k & m2 >= k holds
dist ((seq2 . m1),(seq2 . m2)) < r by A2;
take k ; :: thesis: for b1, b2 being set holds
( not k <= b1 or not k <= b2 or not r <= dist ((seq1 . b1),(seq1 . b2)) )

let m1, m2 be Nat; :: thesis: ( not k <= m1 or not k <= m2 or not r <= dist ((seq1 . m1),(seq1 . m2)) )
reconsider p = (seq2 . m1) - (seq2 . m2) as Element of REAL n by Def6;
- (seq1 . m2) = - (seq2 . m2) by ;
then A4: p = (seq1 . m1) - (seq1 . m2) by ;
assume ( m1 >= k & m2 >= k ) ; :: thesis: not r <= dist ((seq1 . m1),(seq1 . m2))
then A5: dist ((seq2 . m1),(seq2 . m2)) < r by A3;
||.((seq2 . m1) - (seq2 . m2)).|| = sqrt (() . (p,p)) by Def6
.= sqrt (Sum (mlt (p,p))) by Def5
.= sqrt |(p,p)| by RVSUM_1:def 16
.= |.p.| by EUCLID_2:5
.= ||.((seq1 . m1) - (seq1 . m2)).|| by ;
hence not r <= dist ((seq1 . m1),(seq1 . m2)) by A5; :: thesis: verum