theorem Th18: :: ABSVALUE:18

for x, y being Real holds sgn (x * y) = (sgn x) * (sgn y)