theorem Th16: :: NUMBER19:16

for n, k, b being Nat st b > 1 & k > 0 holds
value (((n --> (b -' 1)) ^ (digits ((k -' 1),b))),b) = (k * (b |^ n)) - 1