for X, Z being non empty set
for F being Functional_Sequence of X,REAL st Z common_on_dom F holds
for a, r being positive Real st r < 1 & ( for n being Nat holds (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) ) holds
for z being Element of Z holds
( (lim (F,Z)) . z >= ((F . 0) . z) - (a / (1 - r)) & (lim (F,Z)) . z <= ((F . 0) . z) + (a / (1 - r)) )