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; :: thesis:
let f be Function of Z,REAL; :: thesis:
A2: dom f = Z by FUNCT_2:def 1;
Z c= dom (F . 0) by A1;
then reconsider g = f as PartFunc of X,REAL by A2, RELSET_1:5, XBOOLE_1:1;
assume A3: r < 1 ; :: thesis:
assume A4: for n being Nat holds (F . n) - f,Z is_absolutely_bounded_by a * (r to_power n) ; :: thesis:

A5: now :: thesis:

let x be Element of X; :: thesis:
assume A6: x in Z ; :: thesis:
let p be Real; :: thesis:
assume A7: p > 0 ; :: thesis:
consider k being Element of NAT such that
A8: k >= 1 + (log (r,((p * (1 - r)) / a))) by MESFUNC1:8;
k > log (r,((p * (1 - r)) / a)) by A8, XREAL_1:39;
then A9: r to_power k < r to_power (log (r,((p * (1 - r)) / a))) by A3, POWER:40;
A10: ( a * ((p * (1 - r)) / a) = (p * (1 - r)) * (a / a) & a / a = 1 ) by XCMPLX_1:60, XCMPLX_1:75;
A11: 1 - r > 0 by A3, XREAL_1:50;
then p * (1 - r) > 0 by A7, XREAL_1:129;
then (p * (1 - r)) / a > 0 by XREAL_1:139;
then r to_power k < (p * (1 - r)) / a by A3, A9, POWER:def 3;
then a * (r to_power k) < a * ((p * (1 - r)) / a) by XREAL_1:68;
then (a * (r to_power k)) / (1 - r) < (p * (1 - r)) / (1 - r) by A11, A10, XREAL_1:74;
then A12: (a * (r to_power k)) / (1 - r) < p by A11, XCMPLX_1:89;
reconsider k = k as Nat ;
take k = k; :: thesis:
let n be Nat; :: thesis:
Z c= dom (F . n) by A1;
then x in (dom (F . n)) /\ (dom f) by A2, A6, XBOOLE_0:def 4;
then A13: x in dom ((F . n) - f) by VALUED_1:12;
then A14: ((F . n) - f) . x = ((F . n) . x) - (f . x) by VALUED_1:13;
assume n >= k ; :: thesis:
then ( n = k or n > k ) by XXREAL_0:1;
then r to_power n <= r to_power k by A3, POWER:40;
then A15: a * (r to_power n) <= a * (r to_power k) by XREAL_1:64;
A16: (F . n) - f,Z is_absolutely_bounded_by a * (r to_power n) by A4;
r to_power n >= 0 by POWER:34;
then (a * (r to_power n)) * (1 - r) <= (a * (r to_power n)) * 1 by XREAL_1:43, XREAL_1:64;
then A17: (a * (r to_power n)) / 1 <= (a * (r to_power n)) / (1 - r) by A11, XREAL_1:102;
1 - r > 1 - 1 by A3, XREAL_1:10;
then (a * (r to_power n)) / (1 - r) <= (a * (r to_power k)) / (1 - r) by A15, XREAL_1:72;
then A18: a * (r to_power n) <= (a * (r to_power k)) / (1 - r) by A17, XXREAL_0:2;
x in Z /\ (dom ((F . n) - f)) by A13, XBOOLE_0:def 4;
then |.(((F . n) . x) - (f . x)).| <= a * (r to_power n) by A14, A16;
then |.(((F . n) . x) - (g . x)).| <= (a * (r to_power k)) / (1 - r) by A18, XXREAL_0:2;
hence |.(((F . n) . x) - (g . x)).| < p by A12, XXREAL_0:2; :: thesis:

end;

thus A19: F is_point_conv_on Z :: thesis:

proof

thus Z common_on_dom F by A1; :: according to SEQFUNC:def 11 :: 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 object holds
( b₂ <= 0 or ex b₃ being set st
for b₄ being set holds
( not b₃ <= b₄ or not b₂ <= |.(((F . b₄) . b₁) - (g . b₁)).| ) ) ) by A5; :: thesis:

end;

now :: thesis:

let x be Element of X; :: thesis:
assume A20: x in dom g ; :: thesis:
A21: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((F # x) . m) - (g . x)).| < p

proof

let p be Real; :: thesis:
reconsider p9 = p as Real ;
assume 0 < p ; :: thesis:
then consider n being Nat such that
A22: for m being Nat st n <= m holds
|.(((F . m) . x) - (g . x)).| < p9 by A2, A5, A20;
reconsider n = n as Nat ;
take n ; :: thesis:
let m be Nat; :: thesis:
(F . m) . x = (F # x) . m by SEQFUNC:def 10;
hence ( n <= m implies |.(((F # x) . m) - (g . x)).| < p ) by A22; :: thesis:

end;

F # x is convergent by A2, A19, A20, SEQFUNC:20;
hence g . x = lim (F # x) by A21, SEQ_2:def 7; :: thesis:

end;

hence lim (F,Z) = f by A2, A19, SEQFUNC:def 13; :: thesis: