theorem Th55: :: NUMBER17:55

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