thus Sum (digits (703,10)) = (Sum <%3,0%>) + (Sum <%7%>) by Th339, AFINSQ_2:55
.= (3 + 0) + (Sum <%7%>) by AFINSQ_2:54
.= 3 + 7 by AFINSQ_2:53
.= 10 ; :: thesis: verum