let seq be Complex_Sequence; :: thesis: ( seq is convergent implies for p being Real st 0 < p holds
ex n being Nat st
for m, l being 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 Nat st
for m, l being Nat st n <= m & n <= l holds
|.((seq . m) - (seq . l)).| < p
let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m, l being Nat st n <= m & n <= l holds
|.((seq . m) - (seq . l)).| < p )
assume 0 < p ; :: thesis: ex n being Nat st
for m, l being Nat st n <= m & n <= l holds
|.((seq . m) - (seq . l)).| < p
then consider n being Nat such that
A2: for m being Nat st n <= m holds
|.((seq . m) - (seq . n)).| < p / 2 by A1, Th46;
take n ; :: thesis: for m, l being Nat st n <= m & n <= l holds
|.((seq . m) - (seq . l)).| < p
let m, l be 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:8;
|.(((seq . m) - (seq . n)) - ((seq . l) - (seq . n))).| <= |.((seq . m) - (seq . n)).| + |.((seq . l) - (seq . n)).| by COMPLEX1:57;
hence |.((seq . m) - (seq . l)).| < p by A3, XXREAL_0:2; :: thesis: verum