thus Sum (digits (4500,10)) =
(Sum <%0,0,5%>) + (Sum <%4%>)
by Th1337, AFINSQ_2:55
.=
((Sum <%0,0%>) + (Sum <%5%>)) + (Sum <%4%>)
by AFINSQ_2:55
.=
((0 + 0) + (Sum <%5%>)) + (Sum <%4%>)
by AFINSQ_2:54
.=
((0 + 0) + 5) + (Sum <%4%>)
by AFINSQ_2:53
.=
5 + 4
by AFINSQ_2:53
.=
9
; verum