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
for f being Function of Z,REAL st r < 1 & ( for n being Nat holds (F . n) - f,Z is_absolutely_bounded_by a * (r to_power n) ) holds
( F is_point_conv_on Z & lim (F,Z) = f )