let X, Z be 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)) )
let F be Functional_Sequence of X,REAL; ( Z common_on_dom F implies 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)) ) )
assume A1:
Z common_on_dom F
; 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)) )
let a, r be positive Real; ( r < 1 & ( for n being Nat holds (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) ) implies 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)) ) )
assume A2:
r < 1
; ( ex n being Nat st not (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) or 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)) ) )
assume A3:
for n being Nat holds (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n)
; 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)) )
then
F is_point_conv_on Z
by A1, A2, Th9, SEQFUNC:22;
then A4:
dom (lim (F,Z)) = Z
by SEQFUNC:def 13;
r to_power 0 = 1
by POWER:24;
then A5:
(lim (F,Z)) - (F . 0),Z is_absolutely_bounded_by (a * 1) / (1 - r)
by A1, A2, A3, Th9;
let z be Element of Z; ( (lim (F,Z)) . z >= ((F . 0) . z) - (a / (1 - r)) & (lim (F,Z)) . z <= ((F . 0) . z) + (a / (1 - r)) )
( z in Z & Z c= dom (F . 0) )
by A1;
then
z in (dom (lim (F,Z))) /\ (dom (F . 0))
by A4, XBOOLE_0:def 4;
then A6:
z in dom ((lim (F,Z)) - (F . 0))
by VALUED_1:12;
then
z in Z /\ (dom ((lim (F,Z)) - (F . 0)))
by XBOOLE_0:def 4;
then
|.(((lim (F,Z)) - (F . 0)) . z).| <= (a * 1) / (1 - r)
by A5;
then
|.(((lim (F,Z)) . z) - ((F . 0) . z)).| <= (a * 1) / (1 - r)
by A6, VALUED_1:13;
hence
( (lim (F,Z)) . z >= ((F . 0) . z) - (a / (1 - r)) & (lim (F,Z)) . z <= ((F . 0) . z) + (a / (1 - r)) )
by Th1; verum