theorem Th30: :: NAT_5:30

for n, p being Nat st p is prime holds
sigma (p |^ n) = ((p |^ (n + 1)) - 1) / (p - 1)