theorem Th54: :: NUMBER17:54
for n, b being Nat st n > 0 & b > 1 holds
digits ((n * b),b) = <%0%> ^ (digits (n,b))