theorem :: COMSEQ_3:65

for seq being Complex_Sequence
for z being Complex st |.z.| < 1 & ( for n being Nat holds seq . (n + 1) = z * (seq . n) ) holds
( seq is summable & Sum seq = (seq . 0) / (1r - z) )