thus Sum (digits (78,10)) = (Sum <%8%>) + (Sum <%7%>) by Th111, AFINSQ_2:55
.= 8 + (Sum <%7%>) by AFINSQ_2:53
.= 8 + 7 by AFINSQ_2:53
.= 15 ; :: thesis: verum