let f be Real_Sequence; :: thesis: for a, r being positive real number st r < 1 & ( for n being natural number holds |.((f . n) - (f . (n + 1))).| <= a * (r to_power n) ) holds
( f is convergent & ( for n being natural number holds |.((lim f) - (f . n)).| <= (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))).| <= a * (r to_power n) ) implies ( f is convergent & ( for n being natural number holds |.((lim f) - (f . n)).| <= (a * (r to_power n)) / (1 - r) ) ) )
deffunc H₁( Nat, Real) -> Element of REAL = (f . ($1 + 1)) - (f . $1);
consider g being Function of NAT,REAL such that
A1: ( g . 0 = f . 0 & ( for n being Nat holds g . (n + 1) = H₁(n,g . n) ) ) from NAT_1:sch 12();

now

let n be Element of NAT ; :: thesis: f . (n + 1) = (f . n) + (g . (n + 1))
thus f . (n + 1) = ((f . (n + 1)) - (f . n)) + (f . n)
.= (f . n) + (g . (n + 1)) by A1 ; :: thesis: verum

end;

then A2: f = Partial_Sums g by A1, SERIES_1:def 1;

A3: now

let n be Element of NAT ; :: thesis: 0 <= (abs g) . n
(abs g) . n = abs (g . n) by SEQ_1:12;
hence 0 <= (abs g) . n by COMPLEX1:46; :: thesis: verum

end;

A4: |.r.| = r by COMPLEX1:43;
assume A5: r < 1 ; :: thesis: ( ex n being natural number st not |.((f . n) - (f . (n + 1))).| <= a * (r to_power n) or ( f is convergent & ( for n being natural number holds |.((lim f) - (f . n)).| <= (a * (r to_power n)) / (1 - r) ) ) )
then A6: r GeoSeq is summable by A4, SERIES_1:24;
assume A7: for n being natural number holds |.((f . n) - (f . (n + 1))).| <= a * (r to_power n) ; :: thesis: ( f is convergent & ( for n being natural number holds |.((lim f) - (f . n)).| <= (a * (r to_power n)) / (1 - r) ) )

A8: now

let n be Element of NAT ; :: thesis: ( 1 <= n implies (abs g) . n <= ((a * (r ")) (#) (r GeoSeq)) . n )
set m = 1;
assume 1 <= n ; :: thesis: (abs g) . n <= ((a * (r ")) (#) (r GeoSeq)) . n
then consider k being Nat such that
A9: n = 1 + k by NAT_1:10;
g . n = H₁(k,g . k) by A1, A9;
then (abs g) . n = |.((f . n) - (f . k)).| by A9, SEQ_1:12
.= |.((f . k) - (f . n)).| by COMPLEX1:60 ;
then A10: (abs g) . n <= a * (r to_power k) by A7, A9;
(a * 1) * (r to_power k) = (a * ((r ") * r)) * (r to_power k) by XCMPLX_0:def 7
.= (a * (r ")) * (r * (r to_power k))
.= (a * (r ")) * ((r to_power 1) * (r to_power k)) by POWER:25
.= (a * (r ")) * (r to_power n) by A9, POWER:27
.= (a * (r ")) * (r |^ n) by POWER:41
.= (a * (r ")) * ((r GeoSeq) . n) by PREPOWER:def 1 ;
hence (abs g) . n <= ((a * (r ")) (#) (r GeoSeq)) . n by A10, SEQ_1:9; :: thesis: verum

end;

(a * (r ")) (#) (r GeoSeq) is summable by A6, SERIES_1:10;
then abs g is summable by A3, A8, SERIES_1:19;
then A11: g is absolutely_summable by SERIES_1:def 4;
then g is summable by SERIES_1:35;
hence f is convergent by A2, SERIES_1:def 2; :: thesis: for n being natural number holds |.((lim f) - (f . n)).| <= (a * (r to_power n)) / (1 - r)
let n be natural number ; :: thesis: |.((lim f) - (f . n)).| <= (a * (r to_power n)) / (1 - r)
reconsider n9 = n as Element of NAT by ORDINAL1:def 12;

A12: now

let k be Element of NAT ; :: thesis: ( 0 <= (abs (g ^\ (n9 + 1))) . k & (abs (g ^\ (n9 + 1))) . k <= ((a * (r to_power n)) (#) (r GeoSeq)) . k )
(abs (g ^\ (n9 + 1))) . k = |.((g ^\ (n9 + 1)) . k).| by SEQ_1:12;
hence 0 <= (abs (g ^\ (n9 + 1))) . k by COMPLEX1:46; :: thesis: (abs (g ^\ (n9 + 1))) . k <= ((a * (r to_power n)) (#) (r GeoSeq)) . k
(abs (g ^\ (n9 + 1))) . k = |.((g ^\ (n9 + 1)) . k).| by SEQ_1:12
.= |.(g . ((n9 + 1) + k)).| by NAT_1:def 3
.= |.((f . ((n9 + k) + 1)) - (f . (n9 + k))).| by A1
.= |.((f . (n9 + k)) - (f . ((n9 + k) + 1))).| by UNIFORM1:11 ;
then (abs (g ^\ (n9 + 1))) . k <= a * (r to_power (n9 + k)) by A7;
then (abs (g ^\ (n9 + 1))) . k <= a * ((r to_power n9) * (r to_power k)) by POWER:27;
then (abs (g ^\ (n9 + 1))) . k <= (a * (r to_power n9)) * (r to_power k) ;
then (abs (g ^\ (n9 + 1))) . k <= (a * (r to_power n9)) * (r |^ k) by POWER:41;
then (abs (g ^\ (n9 + 1))) . k <= (a * (r to_power n9)) * ((r GeoSeq) . k) by PREPOWER:def 1;
hence (abs (g ^\ (n9 + 1))) . k <= ((a * (r to_power n)) (#) (r GeoSeq)) . k by SEQ_1:9; :: thesis: verum

end;

A13: (a * (r to_power n)) (#) (r GeoSeq) is summable by A6, SERIES_1:10;
then abs (g ^\ (n9 + 1)) is summable by A12, SERIES_1:20;
then A14: g ^\ (n9 + 1) is absolutely_summable by SERIES_1:def 4;
lim f = Sum g by A2, SERIES_1:def 3;
then lim f = (f . n) + (Sum (g ^\ (n9 + 1))) by A2, A11, SERIES_1:15, SERIES_1:35;
then A15: |.((lim f) - (f . n)).| <= Sum (abs (g ^\ (n9 + 1))) by A14, Th8;
A16: Sum (abs (g ^\ (n9 + 1))) <= Sum ((a * (r to_power n)) (#) (r GeoSeq)) by A13, A12, SERIES_1:20;
Sum ((a * (r to_power n)) (#) (r GeoSeq)) = (a * (r to_power n)) * (Sum (r GeoSeq)) by A6, SERIES_1:10
.= (a * (r to_power n)) * (1 / (1 - r)) by A5, A4, SERIES_1:24
.= (a * (r to_power n)) / (1 - r) by XCMPLX_1:99 ;
hence |.((lim f) - (f . n)).| <= (a * (r to_power n)) / (1 - r) by A16, A15, XXREAL_0:2; :: thesis: verum