theorem Th1: :: SERIES_1:1

for a being Real
for s being Real_Sequence st 0 < a & a < 1 & ( for n being Nat holds s . n = a to_power (n + 1) ) holds
( s is convergent & lim s = 0 )