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

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

seq2 is Cauchy

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

seq2 is Cauchy

let seq2 be sequence of (REAL-US n); :: thesis: ( seq1 = seq2 & seq1 is Cauchy_sequence_by_Norm implies seq2 is Cauchy )

assume that

A1: seq1 = seq2 and

A2: seq1 is Cauchy_sequence_by_Norm ; :: thesis: seq2 is Cauchy

let r be Real; :: according to BHSP_3:def 1 :: 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 ((seq2 . b_{2}),(seq2 . b_{3})) ) )

assume A3: 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 ((seq2 . b_{2}),(seq2 . b_{3})) )

reconsider r = r as Real ;

r > 0 by A3;

then consider k being Nat such that

A4: for n, m being Nat st n >= k & m >= k holds

dist ((seq1 . n),(seq1 . m)) < 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 ((seq2 . b_{1}),(seq2 . b_{2})) )

let m1, m2 be Nat; :: thesis: ( not k <= m1 or not k <= m2 or not r <= dist ((seq2 . m1),(seq2 . m2)) )

reconsider p = (seq2 . m1) - (seq2 . m2) as Element of REAL n by Def6;

- (seq1 . m2) = - (seq2 . m2) by A1, Th13;

then (seq1 . m1) + (- (seq1 . m2)) = (seq2 . m1) + (- (seq2 . m2)) by A1, Th13;

then A5: ||.((seq1 . m1) - (seq1 . m2)).|| = |.p.| by Th1

.= sqrt |(p,p)| by EUCLID_2:5

.= sqrt (Sum (mlt (p,p))) by RVSUM_1:def 16

.= sqrt ((Euclid_scalar n) . (p,p)) by Def5

.= ||.((seq2 . m1) - (seq2 . m2)).|| by Def6 ;

assume ( m1 >= k & m2 >= k ) ; :: thesis: not r <= dist ((seq2 . m1),(seq2 . m2))

then dist ((seq1 . m1),(seq1 . m2)) < r by A4;

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

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

seq2 is Cauchy

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

seq2 is Cauchy

let seq2 be sequence of (REAL-US n); :: thesis: ( seq1 = seq2 & seq1 is Cauchy_sequence_by_Norm implies seq2 is Cauchy )

assume that

A1: seq1 = seq2 and

A2: seq1 is Cauchy_sequence_by_Norm ; :: thesis: seq2 is Cauchy

let r be Real; :: according to BHSP_3:def 1 :: thesis: ( r <= 0 or ex b

for b

( not b

assume A3: r > 0 ; :: thesis: ex b

for b

( not b

reconsider r = r as Real ;

r > 0 by A3;

then consider k being Nat such that

A4: for n, m being Nat st n >= k & m >= k holds

dist ((seq1 . n),(seq1 . m)) < 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 ((seq2 . m1),(seq2 . m2)) )

reconsider p = (seq2 . m1) - (seq2 . m2) as Element of REAL n by Def6;

- (seq1 . m2) = - (seq2 . m2) by A1, Th13;

then (seq1 . m1) + (- (seq1 . m2)) = (seq2 . m1) + (- (seq2 . m2)) by A1, Th13;

then A5: ||.((seq1 . m1) - (seq1 . m2)).|| = |.p.| by Th1

.= sqrt |(p,p)| by EUCLID_2:5

.= sqrt (Sum (mlt (p,p))) by RVSUM_1:def 16

.= sqrt ((Euclid_scalar n) . (p,p)) by Def5

.= ||.((seq2 . m1) - (seq2 . m2)).|| by Def6 ;

assume ( m1 >= k & m2 >= k ) ; :: thesis: not r <= dist ((seq2 . m1),(seq2 . m2))

then dist ((seq1 . m1),(seq1 . m2)) < r by A4;

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