let b be Nat; :: thesis: ( b > 1 implies Sum ((1 / b) GeoSeq) = b / (b - 1) )
assume A0: b > 1 ; :: thesis: Sum ((1 / b) GeoSeq) = b / (b - 1)
then A1: |.(1 / b).| < 1 by Th9;
Sum ((1 / b) GeoSeq) = 1 / (1 - (1 / b)) by A1, SERIES_1:24
.= 1 / ((b / b) - (1 / b)) by XCMPLX_1:60, A0
.= 1 / ((b - 1) / b) by XCMPLX_1:120
.= b / (b - 1) by XCMPLX_1:57 ;
hence Sum ((1 / b) GeoSeq) = b / (b - 1) ; :: thesis: verum