let X be RealUnitarySpace; :: thesis: for seq being sequence of X st seq is V8() holds
seq is Cauchy
let seq be sequence of X; :: thesis: ( seq is V8() implies seq is Cauchy )
assume A1: seq is V8() ; :: thesis: seq is Cauchy
let r be Real; :: according to BHSP_3:def 1 :: thesis: ( r > 0 implies ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
dist (seq . n),(seq . m) < r )
assume A2: r > 0 ; :: thesis: ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
dist (seq . n),(seq . m) < r
take k = 0 ; :: thesis: for n, m being Element of NAT st n >= k & m >= k holds
dist (seq . n),(seq . m) < r
let n, m be Element of NAT ; :: thesis: ( n >= k & m >= k implies dist (seq . n),(seq . m) < r )
assume that
n >= k and
m >= k ; :: thesis: dist (seq . n),(seq . m) < r
dist (seq . n),(seq . m) = dist (seq . n),(seq . n) by A1, VALUED_0:23
.= 0 by BHSP_1:41 ;
hence dist (seq . n),(seq . m) < r by A2; :: thesis: verum