let x be Real; :: thesis: signum . (- x) = - (signum . x)

per cases ( x < 0 or 0 < x or x = 0 ) ;

suppose A1: x < 0 ; :: thesis: signum . (- x) = - (signum . x)

then signum . x = - 1 by Th57;
hence signum . (- x) = - (signum . x) by A1, Th56; :: thesis: verum

end;

suppose A2: 0 < x ; :: thesis: signum . (- x) = - (signum . x)

then signum . x = 1 by Th56;
hence signum . (- x) = - (signum . x) by A2, Th57; :: thesis: verum

end;

suppose x = 0 ; :: thesis: signum . (- x) = - (signum . x)

hence signum . (- x) = - (signum . x) by Th58; :: thesis: verum

end;

end;