let n be Element of 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 CCauchy
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 CCauchy
let seq2 be sequence of (REAL-US n); :: thesis: ( seq1 = seq2 & seq2 is Cauchy implies seq1 is CCauchy )
assume that
A1: seq1 = seq2 and
A2: seq2 is Cauchy ; :: thesis: seq1 is CCauchy
let r be Real; :: according to RSSPACE3:def 5 :: thesis: ( r <= 0 or ex b₁ being Element of NAT st
for b₂, b₃ being Element of NAT holds
( not b₁ <= b₂ or not b₁ <= b₃ or not r <= dist (seq1 . b₂),(seq1 . b₃) ) )
assume r > 0 ; :: thesis: ex b₁ being Element of NAT st
for b₂, b₃ being Element of NAT holds
( not b₁ <= b₂ or not b₁ <= b₃ or not r <= dist (seq1 . b₂),(seq1 . b₃) )
then consider k being Element of NAT such that
A3: for m1, m2 being Element of NAT st m1 >= k & m2 >= k holds
dist (seq2 . m1),(seq2 . m2) < r by A2, BHSP_3:def 1;
take k ; :: thesis: for b₁, b₂ being Element of NAT holds
( not k <= b₁ or not k <= b₂ or not r <= dist (seq1 . b₁),(seq1 . b₂) )
let m1, m2 be Element of 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 17
.= |.p.| by EUCLID_2:13
.= ||.((seq1 . m1) - (seq1 . m2)).|| by A4, Th1 ;
hence not r <= dist (seq1 . m1),(seq1 . m2) by A5; :: thesis: verum