thus Sum (digits (44,10)) = (Sum <%4%>) + (Sum <%4%>) by Th61, AFINSQ_2:55
.= 4 + (Sum <%4%>) by AFINSQ_2:53
.= 4 + 4 by AFINSQ_2:53
.= 8 ; :: thesis: verum