theorem Th419: :: NUMBER11:419

Sum (digits (900,10)) = 9