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