let NRM be non empty ComplexNormSpace; :: thesis: for seq being sequence of NRM holds
( seq is CCauchy iff for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r )
let seq be sequence of NRM; :: thesis: ( seq is CCauchy iff for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r )
thus ( seq is CCauchy implies for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r ) :: thesis: ( ( for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r ) implies seq is CCauchy )

proof

assume A1: seq is CCauchy ; :: thesis: for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r
let r be Real; :: thesis: ( r > 0 implies ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((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
||.((seq . n) - (seq . m)).|| < r
consider k being Element of NAT such that
A3: for n, m being Element of NAT st n >= k & m >= k holds
dist (seq . n),(seq . m) < r by A1, A2, Def5;
for n, m being Element of NAT st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r

proof

let n, m be Element of NAT ; :: thesis: ( n >= k & m >= k implies ||.((seq . n) - (seq . m)).|| < r )
assume A4: ( n >= k & m >= k ) ; :: thesis: ||.((seq . n) - (seq . m)).|| < r
dist (seq . n),(seq . m) < r by A3, A4;
hence ||.((seq . n) - (seq . m)).|| < r ; :: thesis: verum

end;

hence ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r ; :: thesis: verum

end;

thus ( ( for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r ) implies seq is CCauchy ) :: thesis: verum

proof

assume A5: for r being Real st r > 0 holds
ex k being Element of NAT st
for n, m being Element of NAT st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r ; :: thesis: seq is CCauchy

now

let r be Real; :: 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 A6: 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

now

consider k being Element of NAT such that
A7: for n, m being Element of NAT st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r by A5, A6;
for n, m being Element of NAT st n >= k & m >= k holds
dist (seq . n),(seq . m) < r by A7;
hence 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 ; :: thesis: verum

end;

hence 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 ; :: thesis: verum

end;

hence seq is CCauchy by Def5; :: thesis: verum

end;