thus Sum (digits (1672,10)) = (Sum <%2,7,6%>) + (Sum <%1%>) by Th858, AFINSQ_2:55
.= ((Sum <%2,7%>) + (Sum <%6%>)) + (Sum <%1%>) by AFINSQ_2:55
.= ((2 + 7) + (Sum <%6%>)) + (Sum <%1%>) by AFINSQ_2:54
.= ((2 + 7) + 6) + (Sum <%1%>) by AFINSQ_2:53
.= 15 + 1 by AFINSQ_2:53
.= 16 ; :: thesis: verum