theorem Th1148: :: NUMBER11:1148

Sum (digits (1475,10)) = 17