let x be Real; :: thesis: sgn x = sgn (1 / x)
A1: ( 0 < x implies sgn x = sgn (1 / x) )

proof

assume A2: 0 < x ; :: thesis: sgn x = sgn (1 / x)
sgn (1 / x) = 1 / (sgn x) by Th21;
then sgn (1 / x) = 1 / 1 by A2, Def2
.= 1 ;
hence sgn x = sgn (1 / x) by A2, Def2; :: thesis: verum

end;

( x < 0 implies sgn x = sgn (1 / x) )

proof

assume A3: x < 0 ; :: thesis: sgn x = sgn (1 / x)
then sgn x = - 1 by Def2;
then sgn (1 / x) = 1 / (- 1) by Th21;
hence sgn x = sgn (1 / x) by A3, Def2; :: thesis: verum

end;

hence sgn x = sgn (1 / x) by A1; :: thesis: verum