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
( F is_unif_conv_on Z & ( for n being Nat holds (lim (F,Z)) - (F . n),Z is_absolutely_bounded_by (a * (r to_power n)) / (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
( F is_unif_conv_on Z & ( for n being Nat holds (lim (F,Z)) - (F . n),Z is_absolutely_bounded_by (a * (r to_power n)) / (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
( F is_unif_conv_on Z & ( for n being Nat holds (lim (F,Z)) - (F . n),Z is_absolutely_bounded_by (a * (r to_power n)) / (1 - r) ) )
Z c= dom (F . 0) by A1;
then reconsider Z9 = Z as non empty Subset of X by XBOOLE_1:1;
deffunc H₁( Element of Z9) -> Element of REAL = In ((lim (F # $1)),REAL);
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 ( F is_unif_conv_on Z & ( for n being Nat holds (lim (F,Z)) - (F . n),Z is_absolutely_bounded_by (a * (r to_power n)) / (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 ( F is_unif_conv_on Z & ( for n being Nat holds (lim (F,Z)) - (F . n),Z is_absolutely_bounded_by (a * (r to_power n)) / (1 - r) ) ) )
consider f being Function of Z9,REAL such that
A3: for x being Element of Z9 holds f . x = H₁(x) from FUNCT_2:sch 4();
reconsider f = f as PartFunc of X,REAL by RELSET_1:7;
assume A4: for n being Nat holds (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) ; :: thesis: ( F is_unif_conv_on Z & ( for n being Nat holds (lim (F,Z)) - (F . n),Z is_absolutely_bounded_by (a * (r to_power n)) / (1 - r) ) )
thus F is_unif_conv_on Z :: thesis: for n being Nat holds (lim (F,Z)) - (F . n),Z is_absolutely_bounded_by (a * (r to_power n)) / (1 - r)

proof

thus Z common_on_dom F by A1; :: according to SEQFUNC:def 12 :: thesis: ex b₁ being Element of K10(K11(X,REAL)) st
( Z = dom b₁ & ( for b₂ being object holds
( b₂ <= 0 or ex b₃ being set st
for b₄ being set
for b₅ being Element of X holds
( not b₃ <= b₄ or not b₅ in Z or not b₂ <= |.(((F . b₄) . b₅) - (b₁ . b₅)).| ) ) ) )
take f ; :: thesis: ( Z = dom f & ( for b₁ being object holds
( b₁ <= 0 or ex b₂ being set st
for b₃ being set
for b₄ being Element of X holds
( not b₂ <= b₃ or not b₄ in Z or not b₁ <= |.(((F . b₃) . b₄) - (f . b₄)).| ) ) ) )
thus Z = dom f by FUNCT_2:def 1; :: thesis: for b₁ being object holds
( b₁ <= 0 or ex b₂ being set st
for b₃ being set
for b₄ being Element of X holds
( not b₂ <= b₃ or not b₄ in Z or not b₁ <= |.(((F . b₃) . b₄) - (f . b₄)).| ) )
A5: 1 - r > 0 by A2, XREAL_1:50;
let p be Real; :: thesis: ( p <= 0 or ex b₁ being set st
for b₂ being set
for b₃ being Element of X holds
( not b₁ <= b₂ or not b₃ in Z or not p <= |.(((F . b₂) . b₃) - (f . b₃)).| ) )
assume p > 0 ; :: thesis: ex b₁ being set st
for b₂ being set
for b₃ being Element of X holds
( not b₁ <= b₂ or not b₃ in Z or not p <= |.(((F . b₂) . b₃) - (f . b₃)).| )
then p * (1 - r) > 0 by A5, XREAL_1:129;
then A6: (p * (1 - r)) / a > 0 by XREAL_1:139;
consider k being Element of NAT such that
A7: k >= 1 + (log (r,((p * (1 - r)) / a))) by MESFUNC1:8;
A8: ( a * ((p * (1 - r)) / a) = (p * (1 - r)) * (a / a) & a / a = 1 ) by XCMPLX_1:60, XCMPLX_1:75;
k > log (r,((p * (1 - r)) / a)) by A7, XREAL_1:39;
then r to_power k < r to_power (log (r,((p * (1 - r)) / a))) by A2, POWER:40;
then r to_power k < (p * (1 - r)) / a by A2, A6, 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 A5, A8, XREAL_1:74;
then A9: (a * (r to_power k)) / (1 - r) < p by A5, XCMPLX_1:89;
take k ; :: thesis: for b₁ being set
for b₂ being Element of X holds
( not k <= b₁ or not b₂ in Z or not p <= |.(((F . b₁) . b₂) - (f . b₂)).| )
let n be Nat; :: thesis: for b₁ being Element of X holds
( not k <= n or not b₁ in Z or not p <= |.(((F . n) . b₁) - (f . b₁)).| )
let x be Element of X; :: thesis: ( not k <= n or not x in Z or not p <= |.(((F . n) . x) - (f . x)).| )
assume that
A10: n >= k and
A11: x in Z ; :: thesis: not p <= |.(((F . n) . x) - (f . x)).|
A12: ( (F . n) . x = (F # x) . n & |.(((F . n) . x) - (f . x)).| = |.((f . x) - ((F . n) . x)).| ) by COMPLEX1:60, SEQFUNC:def 10;

now :: thesis: for n being Nat holds |.(((F # x) . n) - ((F # x) . (n + 1))).| <= a * (r to_power n)

let n be Nat; :: thesis: |.(((F # x) . n) - ((F # x) . (n + 1))).| <= a * (r to_power n)
A13: (F # x) . n = (F . n) . x by SEQFUNC:def 10;
A14: Z c= dom (F . (n + 1)) by A1;
Z c= dom (F . n) by A1;
then x in (dom (F . n)) /\ (dom (F . (n + 1))) by A11, A14, XBOOLE_0:def 4;
then x in dom ((F . n) - (F . (n + 1))) by VALUED_1:12;
then A15: ( ((F . n) - (F . (n + 1))) . x = ((F . n) . x) - ((F . (n + 1)) . x) & x in Z /\ (dom ((F . n) - (F . (n + 1)))) ) by A11, VALUED_1:13, XBOOLE_0:def 4;
(F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) by A4;
then |.(((F . n) . x) - ((F . (n + 1)) . x)).| <= a * (r to_power n) by A15;
hence |.(((F # x) . n) - ((F # x) . (n + 1))).| <= a * (r to_power n) by A13, SEQFUNC:def 10; :: thesis: verum

end;

then A16: |.((lim (F # x)) - ((F # x) . n)).| <= (a * (r to_power n)) / (1 - r) by A2, Th7;
( n = k or n > k ) by A10, XXREAL_0:1;
then r to_power n <= r to_power k by A2, POWER:40;
then A17: a * (r to_power n) <= a * (r to_power k) by XREAL_1:64;
1 - r > 1 - 1 by A2, XREAL_1:10;
then (a * (r to_power n)) / (1 - r) <= (a * (r to_power k)) / (1 - r) by A17, XREAL_1:72;
then A18: |.((lim (F # x)) - ((F # x) . n)).| <= (a * (r to_power k)) / (1 - r) by A16, XXREAL_0:2;
reconsider xx = x as Element of Z9 by A11;
f . x = H₁(xx) by A3;
hence |.(((F . n) . x) - (f . x)).| < p by A9, A18, A12, XXREAL_0:2; :: thesis: verum

end;

then A19: F is_point_conv_on Z by SEQFUNC:22;
let n9 be Nat; :: thesis: (lim (F,Z)) - (F . n9),Z is_absolutely_bounded_by (a * (r to_power n9)) / (1 - r)
let z be set ; :: according to TIETZE:def 1 :: thesis: ( z in Z /\ (dom ((lim (F,Z)) - (F . n9))) implies |.(((lim (F,Z)) - (F . n9)) . z).| <= (a * (r to_power n9)) / (1 - r) )
reconsider n = n9 as Element of NAT by ORDINAL1:def 12;
assume A20: z in Z /\ (dom ((lim (F,Z)) - (F . n9))) ; :: thesis: |.(((lim (F,Z)) - (F . n9)) . z).| <= (a * (r to_power n9)) / (1 - r)
then reconsider x = z as Element of X ;
A21: z in Z9 by A20, XBOOLE_0:def 4;

now :: thesis: for n being Nat holds |.(((F # x) . n) - ((F # x) . (n + 1))).| <= a * (r to_power n)

let n be Nat; :: thesis: |.(((F # x) . n) - ((F # x) . (n + 1))).| <= a * (r to_power n)
A22: (F # x) . (n + 1) = (F . (n + 1)) . x by SEQFUNC:def 10;
A23: Z c= dom (F . (n + 1)) by A1;
Z c= dom (F . n) by A1;
then z in (dom (F . n)) /\ (dom (F . (n + 1))) by A21, A23, XBOOLE_0:def 4;
then A24: x in dom ((F . n) - (F . (n + 1))) by VALUED_1:12;
then A25: x in Z /\ (dom ((F . n) - (F . (n + 1)))) by A21, XBOOLE_0:def 4;
A26: (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) by A4;
(F # x) . n = (F . n) . x by SEQFUNC:def 10;
then ((F . n) - (F . (n + 1))) . x = ((F # x) . n) - ((F # x) . (n + 1)) by A24, A22, VALUED_1:13;
hence |.(((F # x) . n) - ((F # x) . (n + 1))).| <= a * (r to_power n) by A25, A26; :: thesis: verum

end;

then A27: |.((lim (F # x)) - ((F # x) . n)).| <= (a * (r to_power n)) / (1 - r) by A2, Th7;
Z = dom (lim (F,Z)) by A19, SEQFUNC:def 13;
then |.(((lim (F,Z)) . x) - ((F # x) . n)).| <= (a * (r to_power n)) / (1 - r) by A19, A21, A27, SEQFUNC:def 13;
then A28: |.(((lim (F,Z)) . x) - ((F . n) . x)).| <= (a * (r to_power n)) / (1 - r) by SEQFUNC:def 10;
z in dom ((lim (F,Z)) - (F . n9)) by A20, XBOOLE_0:def 4;
hence |.(((lim (F,Z)) - (F . n9)) . z).| <= (a * (r to_power n9)) / (1 - r) by A28, VALUED_1:13; :: thesis: verum