thus Sum (digits (3175,10)) =
(Sum <%5,7,1%>) + (Sum <%3%>)
by Th1247, AFINSQ_2:55
.=
((Sum <%5,7%>) + (Sum <%1%>)) + (Sum <%3%>)
by AFINSQ_2:55
.=
((5 + 7) + (Sum <%1%>)) + (Sum <%3%>)
by AFINSQ_2:54
.=
((5 + 7) + 1) + (Sum <%3%>)
by AFINSQ_2:53
.=
13 + 3
by AFINSQ_2:53
.=
16
; verum