let rseq be Real_Sequence; :: thesis: ( rseq 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
abs ((rseq . m) - (rseq . l)) < p )
assume A1: rseq 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
abs ((rseq . m) - (rseq . 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
abs ((rseq . m) - (rseq . 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
abs ((rseq . m) - (rseq . l)) < p
then consider n being Element of NAT such that
A2: for m being Element of NAT st n <= m holds
abs ((rseq . m) - (rseq . n)) < p / 2 by A1, SEQ_4:41;
take n ; :: thesis: for m, l being Element of NAT st n <= m & n <= l holds
abs ((rseq . m) - (rseq . l)) < p

now

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

end;

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