let X be RealUnitarySpace; :: thesis: for seq being sequence of X st seq is convergent holds
seq is Cauchy
let seq be sequence of X; :: thesis: ( seq is convergent implies seq is Cauchy )
assume seq is convergent ; :: thesis: seq is Cauchy
then consider h being Point of X such that
A1: for r being Real st r > 0 holds
ex k being Element of NAT st
for n being Element of NAT st n >= k holds
dist (seq . n),h < r by BHSP_2:def 1;
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 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
then r / 2 > 0 by XREAL_1:217;
then consider m1 being Element of NAT such that
A2: for n being Element of NAT st n >= m1 holds
dist (seq . n),h < r / 2 by A1;
take k = m1; :: 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 A3: ( n >= k & m >= k ) ; :: thesis: dist (seq . n),(seq . m) < r
then A4: dist (seq . n),h < r / 2 by A2;
A5: dist (seq . m),h < r / 2 by A2, A3;
A6: dist (seq . n),(seq . m) <= (dist (seq . n),h) + (dist h,(seq . m)) by BHSP_1:42;
(dist (seq . n),h) + (dist h,(seq . m)) < (r / 2) + (r / 2) by A4, A5, XREAL_1:10;
hence dist (seq . n),(seq . m) < r by A6, XXREAL_0:2; :: thesis: verum