let X be ComplexUnitarySpace; :: 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 Nat st
for n being Nat st n >= k holds
dist ((seq . n),h) < r ;
let r be Real; :: according to CLVECT_2:def 8 :: thesis: ( r > 0 implies ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
dist ((seq . n),(seq . m)) < r )
assume r > 0 ; :: thesis: ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
dist ((seq . n),(seq . m)) < r
then consider m1 being Nat such that
A2: for n being Nat st n >= m1 holds
dist ((seq . n),h) < r / 2 by A1, XREAL_1:215;
take k = m1; :: thesis: for n, m being Nat st n >= k & m >= k holds
dist ((seq . n),(seq . m)) < r
let n, m be Nat; :: thesis: ( n >= k & m >= k implies dist ((seq . n),(seq . m)) < r )
assume ( n >= k & m >= k ) ; :: thesis: dist ((seq . n),(seq . m)) < r
then ( dist ((seq . n),h) < r / 2 & dist ((seq . m),h) < r / 2 ) by A2;
then ( dist ((seq . n),(seq . m)) <= (dist ((seq . n),h)) + (dist (h,(seq . m))) & (dist ((seq . n),h)) + (dist (h,(seq . m))) < (r / 2) + (r / 2) ) by CSSPACE:51, XREAL_1:8;
hence dist ((seq . n),(seq . m)) < r by XXREAL_0:2; :: thesis: verum