let f be Real_Sequence; :: thesis: for a, r being positive Real st r < 1 & ( for n being Nat holds |.((f . n) - (f . (n + 1))).| <= a * (r to_power n) ) holds
( f is convergent & ( for n being Nat holds |.((lim f) - (f . n)).| <= (a * (r to_power n)) / (1 - r) ) )
let a, r be positive Real; :: thesis: ( r < 1 & ( for n being Nat holds |.((f . n) - (f . (n + 1))).| <= a * (r to_power n) ) implies ( f is convergent & ( for n being Nat holds |.((lim f) - (f . n)).| <= (a * (r to_power n)) / (1 - r) ) ) )
deffunc H₁( Nat, Real) -> Element of REAL = In (((f . ($1 + 1)) - (f . $1)),REAL);
consider g being sequence of 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 :: thesis: for n being Nat holds f . (n + 1) = (f . n) + (g . (n + 1))

let n be Nat; :: thesis: f . (n + 1) = (f . n) + (g . (n + 1))
A2: g . (n + 1) = H₁(n,g . n) by A1;
thus f . (n + 1) = ((f . (n + 1)) - (f . n)) + (f . n)
.= (f . n) + (g . (n + 1)) by A2 ; :: thesis: verum

end;

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

A4: now :: thesis: for n being Nat holds 0 <= (abs g) . n

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

end;

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

A9: now :: thesis: for n being Nat st 1 <= n holds
(abs g) . n <= ((a * (r ")) (#) (r GeoSeq)) . n

let n be 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
A10: n = 1 + k by NAT_1:10;
g . n = H₁(k,g . k) by A1, A10;
then (abs g) . n = |.((f . n) - (f . k)).| by A10, SEQ_1:12
.= |.((f . k) - (f . n)).| by COMPLEX1:60 ;
then A11: (abs g) . n <= a * (r to_power k) by A8, A10;
(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 A10, 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 A11, SEQ_1:9; :: thesis: verum

end;

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

A13: now :: thesis: for k being Nat holds
( 0 <= (abs (g ^\ (n9 + 1))) . k & (abs (g ^\ (n9 + 1))) . k <= ((a * (r to_power n)) (#) (r GeoSeq)) . k )

let k be Nat; :: thesis: ( 0 <= (abs (g ^\ (n9 + 1))) . k & (abs (g ^\ (n9 + 1))) . k <= ((a * (r to_power n)) (#) (r GeoSeq)) . k )
reconsider kk = k as Element of NAT by ORDINAL1:def 12;
(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
.= |.H₁(n9 + kk,g . n9).| by A1
.= |.((f . ((n9 + k) + 1)) - (f . (n9 + k))).|
.= |.((f . (n9 + k)) - (f . ((n9 + k) + 1))).| by UNIFORM1:11 ;
then (abs (g ^\ (n9 + 1))) . k <= a * (r to_power (n9 + kk)) by A8;
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;

A14: (a * (r to_power n)) (#) (r GeoSeq) is summable by A7, SERIES_1:10;
then abs (g ^\ (n9 + 1)) is summable by A13, SERIES_1:20;
then A15: g ^\ (n9 + 1) is absolutely_summable by SERIES_1:def 4;
lim f = Sum g by A3, SERIES_1:def 3;
then lim f = (f . n) + (Sum (g ^\ (n9 + 1))) by A3, A12, SERIES_1:15;
then A16: |.((lim f) - (f . n)).| <= Sum (abs (g ^\ (n9 + 1))) by A15, Th6;
A17: Sum (abs (g ^\ (n9 + 1))) <= Sum ((a * (r to_power n)) (#) (r GeoSeq)) by A14, A13, SERIES_1:20;
Sum ((a * (r to_power n)) (#) (r GeoSeq)) = (a * (r to_power n)) * (Sum (r GeoSeq)) by A7, SERIES_1:10
.= (a * (r to_power n)) * (1 / (1 - r)) by A6, A5, 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 A17, A16, XXREAL_0:2; :: thesis: verum