thus Sum (digits (4575,10)) =
(Sum <%5,7,5%>) + (Sum <%4%>)
by Th1343, AFINSQ_2:55
.=
((Sum <%5,7%>) + (Sum <%5%>)) + (Sum <%4%>)
by AFINSQ_2:55
.=
((5 + 7) + (Sum <%5%>)) + (Sum <%4%>)
by AFINSQ_2:54
.=
((5 + 7) + 5) + (Sum <%4%>)
by AFINSQ_2:53
.=
17 + 4
by AFINSQ_2:53
.=
21
; verum