let X be ComplexNormSpace; :: 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 A1;

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 Th3, CLVECT_1:def 13;
||.((seq . n) - g1).|| < s / 2 by A2;
then ||.(g1 - (seq . n)).|| < s / 2 by CLVECT_1:108;
then ||.((seq . m) - g1).|| + ||.(g1 - (seq . n)).|| < (s / 2) + (s / 2) by A3, XREAL_1:8;
hence ||.((seq . m) - (seq . n)).|| < s by A4, XXREAL_0:2; :: thesis: verum

end;

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