let b be Nat; :: thesis: ( b > 1 implies digits ((value (<%0%>,b)),b) = <%0%> )
assume A1: b > 1 ; :: thesis: digits ((value (<%0%>,b)),b) = <%0%>
thus digits ((value (<%0%>,b)),b) = digits (0,b) by Th2
.= <%0%> by A1, NUMERAL1:def 2 ; :: thesis: verum