let X, Z be non empty set ; :: thesis:
let F be Functional_Sequence of X,REAL ; :: thesis:
assume A1: Z common_on_dom F ; :: thesis:
let a, r be positive real number ; :: thesis:
let f be Function of Z,REAL ; :: thesis:
assume A2: r < 1 ; :: thesis:
assume A3: for n being natural number holds (F . n) - f,Z is_absolutely_bounded_by a * (r to_power n) ; :: thesis:
A4: dom f = Z by FUNCT_2:def 1;
( Z c= dom (F . 0 ) & dom (F . 0 ) c= X ) by A1, SEQFUNC:def 10;
then reconsider g = f as PartFunc of X,REAL by A4, RELSET_1:13, XBOOLE_1:1;

A5: now

let x be Element of X; :: thesis:
assume A6: x in Z ; :: thesis:
let p be Real; :: thesis:
assume A7: p > 0 ; :: thesis:
A8: 1 - r > 0 by A2, XREAL_1:52;
then p * (1 - r) > 0 by A7, XREAL_1:131;
then A9: (p * (1 - r)) / a > 0 by XREAL_1:141;
consider k being Element of NAT such that
A10: k >= 1 + (log r,((p * (1 - r)) / a)) by MESFUNC1:11;
k > log r,((p * (1 - r)) / a) by A10, XREAL_1:41;
then r to_power k < r to_power (log r,((p * (1 - r)) / a)) by A2, POWER:45;
then ( r to_power k < (p * (1 - r)) / a & a <> 0 ) by A2, A9, POWER:def 3;
then ( a * (r to_power k) < a * ((p * (1 - r)) / a) & a * ((p * (1 - r)) / a) = (p * (1 - r)) * (a / a) & a / a = 1 ) by XCMPLX_1:60, XCMPLX_1:76, XREAL_1:70;
then (a * (r to_power k)) / (1 - r) < (p * (1 - r)) / (1 - r) by A8, XREAL_1:76;
then A11: (a * (r to_power k)) / (1 - r) < p by A8, XCMPLX_1:90;
take k = k; :: thesis:
let n be Element of NAT ; :: thesis:
assume n >= k ; :: thesis:
then ( n = k or n > k ) by XXREAL_0:1;
then r to_power n <= r to_power k by A2, POWER:45;
then ( a * (r to_power n) <= a * (r to_power k) & 1 - r > 1 - 1 ) by A2, XREAL_1:12, XREAL_1:66;
then A12: (a * (r to_power n)) / (1 - r) <= (a * (r to_power k)) / (1 - r) by XREAL_1:74;
Z c= dom (F . n) by A1, SEQFUNC:def 10;
then x in (dom (F . n)) /\ (dom f) by A4, A6, XBOOLE_0:def 4;
then x in dom ((F . n) - f) by VALUED_1:12;
then ( x in Z /\ (dom ((F . n) - f)) & ((F . n) - f) . x = ((F . n) . x) - (f . x) & (F . n) - f,Z is_absolutely_bounded_by a * (r to_power n) ) by A3, A6, VALUED_1:13, XBOOLE_0:def 4;
then A13: |.(((F . n) . x) - (f . x)).| <= a * (r to_power n) by Def1;
r to_power n >= 0 by POWER:39;
then ( 1 - r <= 1 & a * (r to_power n) >= a * 0 ) by XREAL_1:45;
then ( (a * (r to_power n)) * (1 - r) <= (a * (r to_power n)) * 1 & 0 < 1 ) by XREAL_1:66;
then (a * (r to_power n)) / 1 <= (a * (r to_power n)) / (1 - r) by A8, XREAL_1:104;
then a * (r to_power n) <= (a * (r to_power k)) / (1 - r) by A12, XXREAL_0:2;
then abs (((F . n) . x) - (g . x)) <= (a * (r to_power k)) / (1 - r) by A13, XXREAL_0:2;
hence abs (((F . n) . x) - (g . x)) < p by A11, XXREAL_0:2; :: thesis:

end;

thus A14: F is_point_conv_on Z :: thesis:

proof

thus Z common_on_dom F by A1; :: according to SEQFUNC:def 12 :: thesis:
take g ; :: thesis:
thus Z = dom g by FUNCT_2:def 1; :: thesis:
thus for b₁ being Element of X holds
( not b₁ in Z or for b₂ being Element of REAL holds
( b₂ <= 0 or ex b₃ being Element of NAT st
for b₄ being Element of NAT holds
( not b₃ <= b₄ or not b₂ <= abs (((F . b₄) . b₁) - (g . b₁)) ) ) ) by A5; :: thesis:

end;

now

let x be Element of X; :: thesis:
assume A15: x in dom g ; :: thesis:
then A16: F # x is convergent by A4, A14, SEQFUNC:21;
for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((F # x) . m) - (g . x)) < p

proof

let p be real number ; :: thesis:
reconsider p' = p as Real by XREAL_0:def 1;
assume 0 < p ; :: thesis:
then consider n being Element of NAT such that
A17: for m being Element of NAT st n <= m holds
abs (((F . m) . x) - (g . x)) < p' by A4, A5, A15;
take n ; :: thesis:
let m be Element of NAT ; :: thesis:
(F . m) . x = (F # x) . m by SEQFUNC:def 11;
hence ( n <= m implies abs (((F # x) . m) - (g . x)) < p ) by A17; :: thesis:

end;

hence g . x = lim (F # x) by A16, SEQ_2:def 7; :: thesis:

end;

hence lim F,Z = f by A4, A14, SEQFUNC:def 14; :: thesis: