let X be RealNormSpace; :: thesis: for seq being sequence of X holds
( seq is Cauchy_sequence_by_Norm iff for p being Real st p > 0 holds
ex n being Nat st
for m being Nat st n <= m holds
||.((seq . m) - (seq . n)).|| < p )

let seq be sequence of X; :: thesis: ( seq is Cauchy_sequence_by_Norm iff for p being Real st p > 0 holds
ex n being Nat st
for m being Nat st n <= m holds
||.((seq . m) - (seq . n)).|| < p )

A1: now :: thesis: ( ( for p being Real st p > 0 holds
ex n being Nat st
for m being Nat st n <= m holds
||.((seq . m) - (seq . n)).|| < p ) implies seq is Cauchy_sequence_by_Norm )
assume A2: for p being Real st p > 0 holds
ex n being Nat st
for m being Nat st n <= m holds
||.((seq . m) - (seq . n)).|| < p ; :: thesis:
now :: thesis: for s being Real st 0 < s holds
ex k being Nat st
for m, n being Nat st k <= m & k <= n holds
||.((seq . m) - (seq . n)).|| < s
let s be Real; :: thesis: ( 0 < s implies ex k being Nat st
for m, n being Nat st k <= m & k <= n holds
||.((seq . m) - (seq . n)).|| < s )

reconsider ss = s as Real ;
assume 0 < s ; :: thesis: ex k being Nat st
for m, n being Nat st k <= m & k <= n holds
||.((seq . m) - (seq . n)).|| < s

then consider k being Nat such that
A3: for m being Nat st k <= m holds
||.((seq . m) - (seq . k)).|| < ss / 2 by ;
now :: thesis: for m, n being Nat st k <= m & k <= n holds
||.((seq . m) - (seq . n)).|| < s
let m, n be Nat; :: thesis: ( k <= m & k <= n implies ||.((seq . m) - (seq . n)).|| < s )
assume that
A4: k <= m and
A5: k <= n ; :: thesis: ||.((seq . m) - (seq . n)).|| < s
||.((seq . n) - (seq . k)).|| < s / 2 by A3, A5;
then A6: ||.((seq . k) - (seq . n)).|| < s / 2 by NORMSP_1:7;
||.((seq . m) - (seq . k)).|| < s / 2 by A3, A4;
then A7: ||.((seq . m) - (seq . k)).|| + ||.((seq . k) - (seq . n)).|| < (s / 2) + (s / 2) by ;
( ||.(((seq . m) - (seq . k)) + ((seq . k) - (seq . n))).|| <= ||.((seq . m) - (seq . k)).|| + ||.((seq . k) - (seq . n)).|| & ||.(((seq . m) - (seq . k)) + ((seq . k) - (seq . n))).|| = ||.((seq . m) - (seq . n)).|| ) by ;
hence ||.((seq . m) - (seq . n)).|| < s by ; :: thesis: verum
end;
hence ex k being Nat st
for m, n being Nat st k <= m & k <= n holds
||.((seq . m) - (seq . n)).|| < s ; :: thesis: verum
end;
hence seq is Cauchy_sequence_by_Norm by RSSPACE3:8; :: thesis: verum
end;
now :: thesis: ( seq is Cauchy_sequence_by_Norm implies for p being Real st p > 0 holds
ex n being Nat st
for m being Nat st n <= m holds
||.((seq . m) - (seq . n)).|| < p )
assume A8: seq is Cauchy_sequence_by_Norm ; :: thesis: for p being Real st p > 0 holds
ex n being Nat st
for m being Nat st n <= m holds
||.((seq . m) - (seq . n)).|| < p

thus for p being Real st p > 0 holds
ex n being Nat st
for m being Nat st n <= m holds
||.((seq . m) - (seq . n)).|| < p :: thesis: verum
proof
let p be Real; :: thesis: ( p > 0 implies ex n being Nat st
for m being Nat st n <= m holds
||.((seq . m) - (seq . n)).|| < p )

assume p > 0 ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
||.((seq . m) - (seq . n)).|| < p

then consider n being Nat such that
A9: for m, k being Nat st n <= m & n <= k holds
||.((seq . m) - (seq . k)).|| < p by ;
for m being Nat st n <= m holds
||.((seq . m) - (seq . n)).|| < p by A9;
hence ex n being Nat st
for m being Nat st n <= m holds
||.((seq . m) - (seq . n)).|| < p ; :: thesis: verum
end;
end;
hence ( seq is Cauchy_sequence_by_Norm iff for p being Real st p > 0 holds
ex n being Nat st
for m being Nat st n <= m holds
||.((seq . m) - (seq . n)).|| < p ) by A1; :: thesis: verum