theorem Th37: :: COMSEQ_3:37

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