thus Sum (digits (28,10)) = (Sum <%8%>) + (Sum <%2%>) by Th138, AFINSQ_2:55
.= 8 + (Sum <%2%>) by AFINSQ_2:53
.= 8 + 2 by AFINSQ_2:53
.= 10 ; :: thesis: verum