let x be real number ; :: 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 Th44;
hence signum . (- x) = - (signum . x) by Th43, A1; :: thesis: verum

end;

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

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

end;

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

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

end;

end;