let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X holds
( seq is Cauchy iff for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r )
let seq be sequence of X; :: thesis: ( seq is Cauchy iff for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r )
thus ( seq is Cauchy implies for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r ) :: thesis: ( ( for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r ) implies seq is Cauchy )

proof

assume A1: seq is Cauchy ; :: thesis: for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r
let r be Real; :: thesis: ( r > 0 implies ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((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
||.((seq . n) - (seq . m)).|| < r
then consider l being Nat such that
A2: for n, m being Nat st n >= l & m >= l holds
dist ((seq . n),(seq . m)) < r by A1;
take k = l; :: thesis: for n, m being Nat st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r
let n, m be Nat; :: thesis: ( n >= k & m >= k implies ||.((seq . n) - (seq . m)).|| < r )
assume ( n >= k & m >= k ) ; :: thesis: ||.((seq . n) - (seq . m)).|| < r
then dist ((seq . n),(seq . m)) < r by A2;
hence ||.((seq . n) - (seq . m)).|| < r by CSSPACE:def 16; :: thesis: verum

end;

( ( for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r ) implies seq is Cauchy )

proof

assume A3: for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r ; :: thesis: seq is Cauchy
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 l being Nat such that
A4: for n, m being Nat st n >= l & m >= l holds
||.((seq . n) - (seq . m)).|| < r by A3;
take k = l; :: 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 ||.((seq . n) - (seq . m)).|| < r by A4;
hence dist ((seq . n),(seq . m)) < r by CSSPACE:def 16; :: thesis: verum

end;

hence ( ( for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r ) implies seq is Cauchy ) ; :: thesis: verum