thus Sum (digits (1925,10)) =
(Sum <%5,2,9%>) + (Sum <%1%>)
by Th1171, AFINSQ_2:55
.=
((Sum <%5,2%>) + (Sum <%9%>)) + (Sum <%1%>)
by AFINSQ_2:55
.=
((5 + 2) + (Sum <%9%>)) + (Sum <%1%>)
by AFINSQ_2:54
.=
((5 + 2) + 9) + (Sum <%1%>)
by AFINSQ_2:53
.=
16 + 1
by AFINSQ_2:53
.=
17
; verum