let n be Nat; :: thesis: for seq1 being sequence of (REAL-NS n)

for seq2 being sequence of (REAL-US n) st seq1 = seq2 & seq2 is Cauchy holds

seq1 is Cauchy_sequence_by_Norm

let seq1 be sequence of (REAL-NS n); :: thesis: for seq2 being sequence of (REAL-US n) st seq1 = seq2 & seq2 is Cauchy holds

seq1 is Cauchy_sequence_by_Norm

let seq2 be sequence of (REAL-US n); :: 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 b_{1} being set st

for b_{2}, b_{3} being set holds

( not b_{1} <= b_{2} or not b_{1} <= b_{3} or not r <= dist ((seq1 . b_{2}),(seq1 . b_{3})) ) )

assume r > 0 ; :: thesis: ex b_{1} being set st

for b_{2}, b_{3} being set holds

( not b_{1} <= b_{2} or not b_{1} <= b_{3} or not r <= dist ((seq1 . b_{2}),(seq1 . b_{3})) )

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 b_{1}, b_{2} being set holds

( not k <= b_{1} or not k <= b_{2} or not r <= dist ((seq1 . b_{1}),(seq1 . b_{2})) )

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 A1, Th13;

then A4: p = (seq1 . m1) - (seq1 . m2) by A1, Th13;

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 ((Euclid_scalar n) . (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 A4, Th1 ;

hence not r <= dist ((seq1 . m1),(seq1 . m2)) by A5; :: thesis: verum

for seq2 being sequence of (REAL-US n) st seq1 = seq2 & seq2 is Cauchy holds

seq1 is Cauchy_sequence_by_Norm

let seq1 be sequence of (REAL-NS n); :: thesis: for seq2 being sequence of (REAL-US n) st seq1 = seq2 & seq2 is Cauchy holds

seq1 is Cauchy_sequence_by_Norm

let seq2 be sequence of (REAL-US n); :: 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 b

for b

( not b

assume r > 0 ; :: thesis: ex b

for b

( not b

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 b

( not k <= b

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 A1, Th13;

then A4: p = (seq1 . m1) - (seq1 . m2) by A1, Th13;

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 ((Euclid_scalar n) . (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 A4, Th1 ;

hence not r <= dist ((seq1 . m1),(seq1 . m2)) by A5; :: thesis: verum