theorem Th1302: :: NUMBER11:1302

Sum (digits (4050,10)) = 9