thus Sum (digits (4525,10)) =
(Sum <%5,2,5%>) + (Sum <%4%>)
by Th1339, AFINSQ_2:55
.=
((Sum <%5,2%>) + (Sum <%5%>)) + (Sum <%4%>)
by AFINSQ_2:55
.=
((5 + 2) + (Sum <%5%>)) + (Sum <%4%>)
by AFINSQ_2:54
.=
((5 + 2) + 5) + (Sum <%4%>)
by AFINSQ_2:53
.=
12 + 4
by AFINSQ_2:53
.=
16
; verum