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 number st r < 1 & ( for n being natural number 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 number st r < 1 & ( for n being natural number 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 number st r < 1 & ( for n being natural number 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 number ; :: thesis: ( r < 1 & ( for n being natural number 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 natural number 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 natural number 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)) )
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)) )
F is_unif_conv_on Z by A1, A2, A3, Th11;
then F is_point_conv_on Z by SEQFUNC:23;
then ( z in Z & Z c= dom (F . 0 ) & dom (lim F,Z) = Z ) by A1, SEQFUNC:def 10, SEQFUNC:def 14;
then z in (dom (lim F,Z)) /\ (dom (F . 0 )) by XBOOLE_0:def 4;
then A4: ( z in dom ((lim F,Z) - (F . 0 )) & r to_power 0 = 1 ) by POWER:29, VALUED_1:12;
then ( (lim F,Z) - (F . 0 ),Z is_absolutely_bounded_by (a * 1) / (1 - r) & z in Z /\ (dom ((lim F,Z) - (F . 0 ))) ) by A1, A2, A3, Th11, XBOOLE_0:def 4;
then |.(((lim F,Z) - (F . 0 )) . z).| <= (a * 1) / (1 - r) by Def1;
then |.(((lim F,Z) . z) - ((F . 0 ) . z)).| <= (a * 1) / (1 - r) by A4, 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