theorem Th64: :: COMSEQ_3:64

for z being Complex st |.z.| < 1 holds
( z GeoSeq is summable & Sum (z GeoSeq) = 1r / (1r - z) )