for r being Real
for n being Element of NAT st 0 < r & r < 1 holds
Sum ((r GeoSeq) ^\ n) = (r |^ n) / (1 - r)