theorem :: NUMBER11:4
for b being Nat st b > 1 holds
digits ((value (<%0%>,b)),b) = <%0%>