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: seq is Cauchy_sequence_by_Norm

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 A2, XREAL_1:215;

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 A6, XREAL_1:8;
( ||.(((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 Th3, NORMSP_1:def 1;
hence ||.((seq . m) - (seq . n)).|| < s by A7, XXREAL_0:2; :: 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 A8, RSSPACE3:8;
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