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 Element of NAT st
for m being Element of 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 Element of NAT st
for m being Element of 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 Element of NAT st
for m being Element of 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 Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - g1).|| < s by CLVECT_1:def 16;
let s be Real; :: thesis: ( 0 < s implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - (seq . n)).|| < s )
assume 0 < s ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
||.((seq . m) - (seq . n)).|| < s
then 0 < s / 2 by XREAL_1:217;
then consider n being Element of NAT such that
A2: for m being Element of NAT st n <= m holds
||.((seq . m) - g1).|| < s / 2 by A1;

now

let m be Element of NAT ; :: thesis: ( n <= m implies ||.((seq . m) - (seq . n)).|| < s )
assume A3: n <= m ; :: thesis: ||.((seq . m) - (seq . n)).|| < s
||.((seq . n) - g1).|| < s / 2 by A2;
then A4: ||.(g1 - (seq . n)).|| < s / 2 by CLVECT_1:109;
||.((seq . m) - g1).|| < s / 2 by A2, A3;
then A5: ||.((seq . m) - g1).|| + ||.(g1 - (seq . n)).|| < (s / 2) + (s / 2) by A4, XREAL_1:10;
A6: ||.(((seq . m) - g1) + (g1 - (seq . n))).|| <= ||.((seq . m) - g1).|| + ||.(g1 - (seq . n)).|| by CLVECT_1:def 11;
||.(((seq . m) - g1) + (g1 - (seq . n))).|| = ||.((seq . m) - (seq . n)).|| by Th3;
hence ||.((seq . m) - (seq . n)).|| < s by A5, A6, XXREAL_0:2; :: thesis: verum

end;

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