let rseq be Real_Sequence; :: thesis: ( rseq 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
|.((rseq . m) - (rseq . l)).| < p )
assume A1: rseq 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
|.((rseq . m) - (rseq . 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
|.((rseq . m) - (rseq . l)).| < p )
assume 0 < p ; :: thesis: ex n being Nat st
for m, l being Nat st n <= m & n <= l holds
|.((rseq . m) - (rseq . l)).| < p
then consider n being Nat such that
A2: for m being Nat st n <= m holds
|.((rseq . m) - (rseq . n)).| < p / 2 by A1, SEQ_4:41;
take n ; :: thesis: for m, l being Nat st n <= m & n <= l holds
|.((rseq . m) - (rseq . l)).| < p
now :: thesis: for m, l being Nat st n <= m & n <= l holds
|.((rseq . m) - (rseq . l)).| < p
let m, l be Nat; :: thesis: ( n <= m & n <= l implies |.((rseq . m) - (rseq . l)).| < p )
assume ( n <= m & n <= l ) ; :: thesis: |.((rseq . m) - (rseq . l)).| < p
then ( |.((rseq . m) - (rseq . n)).| < p / 2 & |.((rseq . l) - (rseq . n)).| < p / 2 ) by A2;
then A3: |.((rseq . m) - (rseq . n)).| + |.((rseq . l) - (rseq . n)).| < (p / 2) + (p / 2) by XREAL_1:8;
|.((rseq . m) - (rseq . l)).| = |.(((rseq . m) - (rseq . n)) - ((rseq . l) - (rseq . n))).| ;
then |.((rseq . m) - (rseq . l)).| <= |.((rseq . m) - (rseq . n)).| + |.((rseq . l) - (rseq . n)).| by COMPLEX1:57;
hence |.((rseq . m) - (rseq . l)).| < p by A3, XXREAL_0:2; :: thesis: verum
end;
hence for m, l being Nat st n <= m & n <= l holds
|.((rseq . m) - (rseq . l)).| < p ; :: thesis: verum