let NRM be RealNormSpace; :: thesis: for seq being sequence of NRM holds
( seq is Cauchy_sequence_by_Norm 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 NRM; :: thesis: ( seq is Cauchy_sequence_by_Norm 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_sequence_by_Norm 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_sequence_by_Norm )

proof

assume A1: seq is Cauchy_sequence_by_Norm ; :: 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 k being Nat such that
A2: for n, m being Nat st n >= k & m >= k holds
dist ((seq . n),(seq . m)) < r by A1;
for n, m being Nat st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r

proof

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

end;

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

end;

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_sequence_by_Norm

now :: 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
dist ((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
dist ((seq . n),(seq . m)) < r )
assume A4: 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

now :: thesis: ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
dist ((seq . n),(seq . m)) < r

consider k being Nat such that
A5: for n, m being Nat st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r by A3, A4;
for n, m being Nat st n >= k & m >= k holds
dist ((seq . n),(seq . m)) < r by A5;
hence ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
dist ((seq . n),(seq . m)) < r ; :: thesis: verum

end;

hence ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
dist ((seq . n),(seq . m)) < r ; :: thesis: verum

end;

hence seq is Cauchy_sequence_by_Norm ; :: thesis: verum