theorem Th24: :: SERIES_1:24
for a being Real st |.a.| < 1 holds
( a GeoSeq is summable & Sum (a GeoSeq) = 1 / (1 - a) )