let a be Real; :: thesis: ( |.a.| < 1 implies ( a GeoSeq is summable & Sum (a GeoSeq) = 1 / (1 - a) ) )
deffunc H1( Nat) -> object = a to_power ($1 + 1);
consider s being Real_Sequence such that
A1: for n being Nat holds s . n = H1(n) from SEQ_1:sch 1();
 assume A2: |.a.| < 1 ; :: thesis: ( a GeoSeq is summable & Sum (a GeoSeq) = 1 / (1 - a) )
then A3: ( s is convergent & lim s = 0 ) by A1, Th3;
A4: now :: thesis: for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
|.(((Partial_Sums (a GeoSeq)) . n) - (1 / (1 - a))).| < r
a < 1 by A2, SEQ_2:1;
then A5: 1 - a > 0 by XREAL_1:50;
let r be Real; :: thesis: ( r > 0 implies ex m being Nat st
for n being Nat st n >= m holds
|.(((Partial_Sums (a GeoSeq)) . n) - (1 / (1 - a))).| < r )
assume r > 0 ; :: thesis: ex m being Nat st
for n being Nat st n >= m holds
|.(((Partial_Sums (a GeoSeq)) . n) - (1 / (1 - a))).| < r
then r * (1 - a) > 0 * r by A5;
then consider m being Nat such that
A6: for n being Nat st n >= m holds
|.((s . n) - 0).| < r * (1 - a) by A3, SEQ_2:def 7;
take m = m; :: thesis: for n being Nat st n >= m holds
|.(((Partial_Sums (a GeoSeq)) . n) - (1 / (1 - a))).| < r
let n be Nat; :: thesis: ( n >= m implies |.(((Partial_Sums (a GeoSeq)) . n) - (1 / (1 - a))).| < r )
assume n >= m ; :: thesis: |.(((Partial_Sums (a GeoSeq)) . n) - (1 / (1 - a))).| < r
then |.((s . n) - 0).| < r * (1 - a) by A6;
then |.((a to_power (n + 1)) - 0).| < r * (1 - a) by A1;
then A7: |.(a to_power (n + 1)).| / (1 - a) < (r * (1 - a)) / (1 - a) by A5, XREAL_1:74;
a <> 1 by A2, SEQ_2:1;
then A8: |.(((Partial_Sums (a GeoSeq)) . n) - (1 / (1 - a))).| = |.(((1 - (a to_power (n + 1))) / (1 - a)) - (1 / (1 - a))).| by Th22
.= |.(((1 + (- (a to_power (n + 1)))) - 1) / (1 - a)).|
.= |.(- ((a to_power (n + 1)) / (1 - a))).|
.= |.((a to_power (n + 1)) / (1 - a)).| by COMPLEX1:52
.= |.(a to_power (n + 1)).| / |.(1 - a).| by COMPLEX1:67
.= |.(a to_power (n + 1)).| / (1 - a) by A5, ABSVALUE:def 1 ;
1 - a <> 0 by A2, SEQ_2:1;
hence |.(((Partial_Sums (a GeoSeq)) . n) - (1 / (1 - a))).| < r by A8, A7, XCMPLX_1:89; :: thesis: verum
end;
then A9: Partial_Sums (a GeoSeq) is convergent by SEQ_2:def 6;
hence a GeoSeq is summable ; :: thesis: Sum (a GeoSeq) = 1 / (1 - a)
thus Sum (a GeoSeq) = 1 / (1 - a) by A4, A9, SEQ_2:def 7; :: thesis: verum