let X, Z be non empty set ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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) ; :: thesis: 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; :: thesis: ( (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; :: thesis: verum