theorem Th23: :: TOPGEN_3:23

for n being Element of NAT holds Sum (((1 / 2) GeoSeq) ^\ (n + 1)) = (1 / 2) |^ n