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:16;
hence 0 <= (abs g) . n by COMPLEX1:132; :: thesis: verum

end;

A4: |.r.| = r by COMPLEX1:129;
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:28;
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:16
.= |.((f . k) - (f . n)).| by COMPLEX1:146 ;
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:30
.= (a * (r " )) * (r to_power n) by A9, POWER:32
.= (a * (r " )) * (r |^ n) by POWER:46
.= (a * (r " )) * ((r GeoSeq ) . n) by PREPOWER:def 1 ;
hence (abs g) . n <= ((a * (r " )) (#) (r GeoSeq )) . n by A10, SEQ_1:13; :: thesis: verum

end;

(a * (r " )) (#) (r GeoSeq ) is summable by A6, SERIES_1:13;
then abs g is summable by A3, A8, SERIES_1:22;
then A11: g is absolutely_summable by SERIES_1:def 5;
then g is summable by SERIES_1:40;
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 13;

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:16;
hence 0 <= (abs (g ^\ (n9 + 1))) . k by COMPLEX1:132; :: 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:16
.= |.(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:13 ;
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:32;
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:46;
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:13; :: thesis: verum

end;

A13: (a * (r to_power n)) (#) (r GeoSeq ) is summable by A6, SERIES_1:13;
then abs (g ^\ (n9 + 1)) is summable by A12, SERIES_1:24;
then A14: g ^\ (n9 + 1) is absolutely_summable by SERIES_1:def 5;
lim f = Sum g by A2, SERIES_1:def 3;
then lim f = (f . n) + (Sum (g ^\ (n9 + 1))) by A2, A11, SERIES_1:18, SERIES_1:40;
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:24;
Sum ((a * (r to_power n)) (#) (r GeoSeq )) = (a * (r to_power n)) * (Sum (r GeoSeq )) by A6, SERIES_1:13
.= (a * (r to_power n)) * (1 / (1 - r)) by A5, A4, SERIES_1:28
.= (a * (r to_power n)) / (1 - r) by XCMPLX_1:100 ;
hence |.((lim f) - (f . n)).| <= (a * (r to_power n)) / (1 - r) by A16, A15, XXREAL_0:2; :: thesis: verum