theorem :: SERIES_1:25

for a being Real
for s being Real_Sequence st |.a.| < 1 & ( for n being Nat holds s . (n + 1) = a * (s . n) ) holds
( s is summable & Sum s = (s . 0) / (1 - a) )