let seq be Real_Sequence; :: thesis:
assume seq is convergent ; :: thesis:
then consider g being real number such that
A1: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - g) < p by Def6;
consider n1 being Element of NAT such that
A2: for m being Element of NAT st n1 <= m holds
abs ((seq . m) - g) < 1 by A1;

take r = (abs g) + 1; :: thesis:
0 + 0 < r by COMPLEX1:46, XREAL_1:8;
hence 0 < r ; :: thesis:
let m be Element of NAT ; :: thesis:
assume n1 <= m ; :: thesis:
then A4: abs ((seq . m) - g) < 1 by A2;
(abs (seq . m)) - (abs g) <= abs ((seq . m) - g) by COMPLEX1:59;
then A5: (abs (seq . m)) - (abs g) < 1 by A4, XXREAL_0:2;
((abs (seq . m)) - (abs g)) + (abs g) = abs (seq . m) ;
hence abs (seq . m) < r by A5, XREAL_1:6; :: thesis:

end;

consider r1 being real number such that
A6: 0 < r1 and
A7: for m being Element of NAT st n1 <= m holds
abs (seq . m) < r1 by A3;
consider r2 being real number such that
A8: 0 < r2 and
A9: for m being Element of NAT st m <= n1 holds
abs (seq . m) < r2 by Th16;
take r = r1 + r2; :: thesis:
thus 0 < r by A6, A8; :: thesis:
A10: r1 + 0 < r by A8, XREAL_1:8;
A11: 0 + r2 < r by A6, XREAL_1:8;
let m be Element of NAT ; :: thesis:

A12: now

end;

end;

hence abs (seq . m) < r by A12; :: thesis:

end;