thus Sum (digits (68,10)) = (Sum <%8%>) + (Sum <%6%>) by Th227, AFINSQ_2:55
.= 8 + (Sum <%6%>) by AFINSQ_2:53
.= 8 + 6 by AFINSQ_2:53
.= 14 ; :: thesis: verum