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

let seq be sequence of X; :: thesis: ( seq is convergent implies for s being Real st 0 < s holds
ex n being Nat st
for m being Nat st n <= m holds
||.((seq . m) - (seq . n)).|| < s )

assume seq is convergent ; :: thesis: for s being Real st 0 < s holds
ex n being Nat st
for m being Nat st n <= m holds
||.((seq . m) - (seq . n)).|| < s

then consider g1 being Element of X such that
A1: for s being Real st 0 < s holds
ex n being Nat st
for m being Nat st n <= m holds
||.((seq . m) - g1).|| < s ;
let s be Real; :: thesis: ( 0 < s implies ex n being Nat st
for m being Nat st n <= m holds
||.((seq . m) - (seq . n)).|| < s )

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

then consider n being Nat such that
A2: for m being Nat st n <= m holds
||.((seq . m) - g1).|| < s / 2 by ;
now :: thesis: for m being Nat st n <= m holds
||.((seq . m) - (seq . n)).|| < s
let m be Nat; :: thesis: ( n <= m implies ||.((seq . m) - (seq . n)).|| < s )
assume n <= m ; :: thesis: ||.((seq . m) - (seq . n)).|| < s
then A3: ||.((seq . m) - g1).|| < s / 2 by A2;
A4: ( ||.(((seq . m) - g1) + (g1 - (seq . n))).|| <= ||.((seq . m) - g1).|| + ||.(g1 - (seq . n)).|| & ||.(((seq . m) - g1) + (g1 - (seq . n))).|| = ||.((seq . m) - (seq . n)).|| ) by ;
||.((seq . n) - g1).|| < s / 2 by A2;
then ||.(g1 - (seq . n)).|| < s / 2 by NORMSP_1:7;
then ||.((seq . m) - g1).|| + ||.(g1 - (seq . n)).|| < (s / 2) + (s / 2) by ;
hence ||.((seq . m) - (seq . n)).|| < s by ; :: thesis: verum
end;
hence ex n being Nat st
for m being Nat st n <= m holds
||.((seq . m) - (seq . n)).|| < s ; :: thesis: verum