theorem Th320: :: NUMBER11:320

Sum (digits (513,10)) = 9