theorem :: NUMBER19:14
for n, k, b being Nat st b > 1 & k > 0 & n > 0 holds
digits (((k * (b |^ n)) + 1),b) = (<%1%> ^ ((n -' 1) --> 0)) ^ (digits (k,b))