thus Sum (digits (3475,10)) =
(Sum <%5,7,4%>) + (Sum <%3%>)
by Th1265, AFINSQ_2:55
.=
((Sum <%5,7%>) + (Sum <%4%>)) + (Sum <%3%>)
by AFINSQ_2:55
.=
((5 + 7) + (Sum <%4%>)) + (Sum <%3%>)
by AFINSQ_2:54
.=
((5 + 7) + 4) + (Sum <%3%>)
by AFINSQ_2:53
.=
16 + 3
by AFINSQ_2:53
.=
19
; verum