let seq be Complex_Sequence; :: thesis: ( seq is convergent implies for p being Real st 0 < p holds
ex n being Element of NAT st
for m, l being Element of NAT st n <= m & n <= l holds
|.((seq . m) - (seq . l)).| < p )
assume A1: seq is convergent ; :: thesis: for p being Real st 0 < p holds
ex n being Element of NAT st
for m, l being Element of NAT st n <= m & n <= l holds
|.((seq . m) - (seq . l)).| < p
let p be Real; :: thesis: ( 0 < p implies ex n being Element of NAT st
for m, l being Element of NAT st n <= m & n <= l holds
|.((seq . m) - (seq . l)).| < p )
assume 0 < p ; :: thesis: ex n being Element of NAT st
for m, l being Element of NAT st n <= m & n <= l holds
|.((seq . m) - (seq . l)).| < p
then consider n being Element of NAT such that
A2: for m being Element of NAT st n <= m holds
|.((seq . m) - (seq . n)).| < p / 2 by A1, Th46;
take n ; :: thesis: for m, l being Element of NAT st n <= m & n <= l holds
|.((seq . m) - (seq . l)).| < p

now

let m, l be Element of NAT ; :: thesis: ( n <= m & n <= l implies |.((seq . m) - (seq . l)).| < p )
assume ( n <= m & n <= l ) ; :: thesis: |.((seq . m) - (seq . l)).| < p
then ( |.((seq . m) - (seq . n)).| < p / 2 & |.((seq . l) - (seq . n)).| < p / 2 ) by A2;
then A3: |.((seq . m) - (seq . n)).| + |.((seq . l) - (seq . n)).| < (p / 2) + (p / 2) by XREAL_1:10;
|.(((seq . m) - (seq . n)) - ((seq . l) - (seq . n))).| <= |.((seq . m) - (seq . n)).| + |.((seq . l) - (seq . n)).| by COMPLEX1:143;
hence |.((seq . m) - (seq . l)).| < p by A3, XXREAL_0:2; :: thesis: verum

end;

hence for m, l being Element of NAT st n <= m & n <= l holds
|.((seq . m) - (seq . l)).| < p ; :: thesis: verum