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
( F is_unif_conv_on Z & ( for n being natural number 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 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
( F is_unif_conv_on Z & ( for n being natural number 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 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
( F is_unif_conv_on Z & ( for n being natural number holds (lim F,Z) - (F . n),Z is_absolutely_bounded_by (a * (r to_power n)) / (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 ( F is_unif_conv_on Z & ( for n being natural number 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 natural number 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 natural number holds (lim F,Z) - (F . n),Z is_absolutely_bounded_by (a * (r to_power n)) / (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: ( F is_unif_conv_on Z & ( for n being natural number holds (lim F,Z) - (F . n),Z is_absolutely_bounded_by (a * (r to_power n)) / (1 - r) ) )
( Z c= dom (F . 0 ) & dom (F . 0 ) c= X ) by A1, SEQFUNC:def 10;
then reconsider Z' = Z as non empty Subset of X by XBOOLE_1:1;
deffunc H₁( Element of Z') -> Element of REAL = lim (F # $1);
consider f being Function of Z',REAL such that
A4: for x being Element of Z' holds f . x = H₁(x) from FUNCT_2:sch 4();
reconsider f = f as PartFunc of X,REAL by RELSET_1:17;
thus F is_unif_conv_on Z :: thesis: for n being natural number 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 13 :: thesis: ex b₁ being Element of K21(K22(X,REAL )) st
( Z = dom b₁ & ( for b₂ being Element of REAL holds
( b₂ <= 0 or ex b₃ being Element of NAT st
for b₄ being Element of NAT
for b₅ being Element of X holds
( not b₃ <= b₄ or not b₅ in Z or not b₂ <= abs (((F . b₄) . b₅) - (b₁ . b₅)) ) ) ) )
take f ; :: thesis: ( Z = dom f & ( for b₁ being Element of REAL holds
( b₁ <= 0 or ex b₂ being Element of NAT st
for b₃ being Element of NAT
for b₄ being Element of X holds
( not b₂ <= b₃ or not b₄ in Z or not b₁ <= abs (((F . b₃) . b₄) - (f . b₄)) ) ) ) )
thus Z = dom f by FUNCT_2:def 1; :: thesis: for b₁ being Element of REAL holds
( b₁ <= 0 or ex b₂ being Element of NAT st
for b₃ being Element of NAT
for b₄ being Element of X holds
( not b₂ <= b₃ or not b₄ in Z or not b₁ <= abs (((F . b₃) . b₄) - (f . b₄)) ) )
let p be Real; :: thesis: ( p <= 0 or ex b₁ being Element of NAT st
for b₂ being Element of NAT
for b₃ being Element of X holds
( not b₁ <= b₂ or not b₃ in Z or not p <= abs (((F . b₂) . b₃) - (f . b₃)) ) )
assume A5: p > 0 ; :: thesis: ex b₁ being Element of NAT st
for b₂ being Element of NAT
for b₃ being Element of X holds
( not b₁ <= b₂ or not b₃ in Z or not p <= abs (((F . b₂) . b₃) - (f . b₃)) )
A6: 1 - r > 0 by A2, XREAL_1:52;
then p * (1 - r) > 0 by A5, XREAL_1:131;
then A7: (p * (1 - r)) / a > 0 by XREAL_1:141;
consider k being Element of NAT such that
A8: k >= 1 + (log r,((p * (1 - r)) / a)) by MESFUNC1:11;
k > log r,((p * (1 - r)) / a) by A8, 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, A7, 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 A6, XREAL_1:76;
then A9: (a * (r to_power k)) / (1 - r) < p by A6, XCMPLX_1:90;
take k ; :: thesis: for b₁ being Element of NAT
for b₂ being Element of X holds
( not k <= b₁ or not b₂ in Z or not p <= abs (((F . b₁) . b₂) - (f . b₂)) )
let n be Element of NAT ; :: thesis: for b₁ being Element of X holds
( not k <= n or not b₁ in Z or not p <= abs (((F . n) . b₁) - (f . b₁)) )
let x be Element of X; :: thesis: ( not k <= n or not x in Z or not p <= abs (((F . n) . x) - (f . x)) )
assume A10: ( n >= k & x in Z ) ; :: thesis: not p <= abs (((F . n) . x) - (f . x))
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 A11: (a * (r to_power n)) / (1 - r) <= (a * (r to_power k)) / (1 - r) by XREAL_1:74;

now

let n be natural number ; :: thesis: |.(((F # x) . n) - ((F # x) . (n + 1))).| <= a * (r to_power n)
A12: ( n in NAT & n + 1 in NAT ) by ORDINAL1:def 13;
then ( Z c= dom (F . n) & Z c= dom (F . (n + 1)) ) by A1, SEQFUNC:def 10;
then x in (dom (F . n)) /\ (dom (F . (n + 1))) by A10, XBOOLE_0:def 4;
then x in dom ((F . n) - (F . (n + 1))) by VALUED_1:12;
then ( ((F . n) - (F . (n + 1))) . x = ((F . n) . x) - ((F . (n + 1)) . x) & (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) & x in Z /\ (dom ((F . n) - (F . (n + 1)))) ) by A3, A10, VALUED_1:13, XBOOLE_0:def 4;
then ( |.(((F . n) . x) - ((F . (n + 1)) . x)).| <= a * (r to_power n) & (F # x) . n = (F . n) . x & (F # x) . (n + 1) = (F . (n + 1)) . x ) by A12, Def1, SEQFUNC:def 11;
hence |.(((F # x) . n) - ((F # x) . (n + 1))).| <= a * (r to_power n) ; :: thesis: verum

end;

then |.((lim (F # x)) - ((F # x) . n)).| <= (a * (r to_power n)) / (1 - r) by A2, Th9;
then A13: |.((lim (F # x)) - ((F # x) . n)).| <= (a * (r to_power k)) / (1 - r) by A11, XXREAL_0:2;
( (F . n) . x = (F # x) . n & f . x = lim (F # x) & |.(((F . n) . x) - (f . x)).| = |.((f . x) - ((F . n) . x)).| ) by A4, A10, COMPLEX1:146, SEQFUNC:def 11;
hence |.(((F . n) . x) - (f . x)).| < p by A9, A13, XXREAL_0:2; :: thesis: verum

end;

then A14: F is_point_conv_on Z by SEQFUNC:23;
let n' be natural number ; :: thesis: (lim F,Z) - (F . n'),Z is_absolutely_bounded_by (a * (r to_power n')) / (1 - r)
let z be set ; :: according to TIETZE:def 1 :: thesis: ( z in Z /\ (dom ((lim F,Z) - (F . n'))) implies abs (((lim F,Z) - (F . n')) . z) <= (a * (r to_power n')) / (1 - r) )
reconsider n = n' as Element of NAT by ORDINAL1:def 13;
assume A15: z in Z /\ (dom ((lim F,Z) - (F . n'))) ; :: thesis: abs (((lim F,Z) - (F . n')) . z) <= (a * (r to_power n')) / (1 - r)
then A16: ( z in Z' & z in dom ((lim F,Z) - (F . n')) ) by XBOOLE_0:def 4;
reconsider x = z as Element of X by A15;
A17: Z = dom (lim F,Z) by A14, SEQFUNC:def 14;

now

let n be natural number ; :: thesis: |.(((F # x) . n) - ((F # x) . (n + 1))).| <= a * (r to_power n)
A18: ( n in NAT & n + 1 in NAT ) by ORDINAL1:def 13;
then ( Z c= dom (F . n) & Z c= dom (F . (n + 1)) ) by A1, SEQFUNC:def 10;
then z in (dom (F . n)) /\ (dom (F . (n + 1))) by A16, XBOOLE_0:def 4;
then ( x in dom ((F . n) - (F . (n + 1))) & (F # x) . n = (F . n) . x & (F # x) . (n + 1) = (F . (n + 1)) . x ) by A18, SEQFUNC:def 11, VALUED_1:12;
then ( x in Z /\ (dom ((F . n) - (F . (n + 1)))) & (F . n) - (F . (n + 1)),Z is_absolutely_bounded_by a * (r to_power n) & ((F . n) - (F . (n + 1))) . x = ((F # x) . n) - ((F # x) . (n + 1)) ) by A3, A16, VALUED_1:13, XBOOLE_0:def 4;
hence |.(((F # x) . n) - ((F # x) . (n + 1))).| <= a * (r to_power n) by Def1; :: thesis: verum

end;

then |.((lim (F # x)) - ((F # x) . n)).| <= (a * (r to_power n)) / (1 - r) by A2, Th9;
then |.(((lim F,Z) . x) - ((F # x) . n)).| <= (a * (r to_power n)) / (1 - r) by A14, A16, A17, SEQFUNC:def 14;
then |.(((lim F,Z) . x) - ((F . n) . x)).| <= (a * (r to_power n)) / (1 - r) by SEQFUNC:def 11;
hence abs (((lim F,Z) - (F . n')) . z) <= (a * (r to_power n')) / (1 - r) by A16, VALUED_1:13; :: thesis: verum