theorem lempowers: :: NUMBER01:12

for a being Nat
for m being positive Integer
for f being XFinSequence of INT st a > 1 & len f = m - 1 & ( for i being Nat st i in dom f holds
f . i = (a |^ (i + 1)) - 1 ) holds
((a |^ m) - 1) div (a - 1) = (Sum f) + m