let n, b be Nat; :: thesis: ( n < b & b > 1 implies Sum (digits (n,b)) = n )
assume ( n < b & b > 1 ) ; :: thesis: Sum (digits (n,b)) = n
hence Sum (digits (n,b)) = Sum <%n%> by Th3
.= n by AFINSQ_2:53 ;
:: thesis: verum