thus Sum (digits (1584,10)) = (Sum <%4,8,5%>) + (Sum <%1%>) by Th850, AFINSQ_2:55
.= ((Sum <%4,8%>) + (Sum <%5%>)) + (Sum <%1%>) by AFINSQ_2:55
.= ((4 + 8) + (Sum <%5%>)) + (Sum <%1%>) by AFINSQ_2:54
.= ((4 + 8) + 5) + (Sum <%1%>) by AFINSQ_2:53
.= 17 + 1 by AFINSQ_2:53
.= 18 ; :: thesis: verum