for f being Real_Sequence
for a, r being positive Real st r < 1 & ( for n being Nat holds |.((f . n) - (f . (n + 1))).| <= a * (r to_power n) ) holds
( lim f >= (f . 0) - (a / (1 - r)) & lim f <= (f . 0) + (a / (1 - r)) )