thus Sum (digits (4075,10)) =
(Sum <%5,7,0%>) + (Sum <%4%>)
by Th1303, AFINSQ_2:55
.=
((Sum <%5,7%>) + (Sum <%0%>)) + (Sum <%4%>)
by AFINSQ_2:55
.=
((5 + 7) + (Sum <%0%>)) + (Sum <%4%>)
by AFINSQ_2:54
.=
((5 + 7) + 0) + (Sum <%4%>)
by AFINSQ_2:53
.=
12 + 4
by AFINSQ_2:53
.=
16
; verum