theorem Th9: :: TIETZE:9

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
( F is_unif_conv_on Z & ( for n being Nat holds (lim (F,Z)) - (F . n),Z is_absolutely_bounded_by (a * (r to_power n)) / (1 - r) ) )