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₁ being set st
for b₂, b₃ being set holds
( not b₁ <= b₂ or not b₁ <= b₃ or not r <= dist ((seq2 . b₂),(seq2 . b₃)) ) )
assume A3: 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 ((seq2 . b₂),(seq2 . 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₁, b₂ being set holds
( not k <= b₁ or not k <= b₂ or not r <= dist ((seq2 . b₁),(seq2 . 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