theorem Th57: :: FUNCT_8:57

for x being Real st x < 0 holds
signum . x = - 1