thus Sum (digits (4925,10)) =
(Sum <%5,2,9%>) + (Sum <%4%>)
by Th1371, AFINSQ_2:55
.=
((Sum <%5,2%>) + (Sum <%9%>)) + (Sum <%4%>)
by AFINSQ_2:55
.=
((5 + 2) + (Sum <%9%>)) + (Sum <%4%>)
by AFINSQ_2:54
.=
((5 + 2) + 9) + (Sum <%4%>)
by AFINSQ_2:53
.=
16 + 4
by AFINSQ_2:53
.=
20
; verum