thus Sum (digits (99,10)) = (Sum <%9%>) + (Sum <%9%>) by Th71, AFINSQ_2:55
.= 9 + (Sum <%9%>) by AFINSQ_2:53
.= 9 + 9 by AFINSQ_2:53
.= 18 ; :: thesis: verum