thus Sum (digits (1127,10)) = (Sum <%7,2,1%>) + (Sum <%1%>) by Th1001, AFINSQ_2:55
.= ((Sum <%7,2%>) + (Sum <%1%>)) + (Sum <%1%>) by AFINSQ_2:55
.= ((7 + 2) + (Sum <%1%>)) + (Sum <%1%>) by AFINSQ_2:54
.= ((7 + 2) + 1) + (Sum <%1%>) by AFINSQ_2:53
.= 10 + 1 by AFINSQ_2:53
.= 11 ; :: thesis: verum