let x be Real; :: thesis: ( x <> 0 implies (sgn x) * (sgn (1 / x)) = 1 )
assume x <> 0 ; :: thesis: (sgn x) * (sgn (1 / x)) = 1
then sgn (x * (1 / x)) = sgn 1 by XCMPLX_1:106;
then sgn (x * (1 / x)) = 1 by Def2;
hence (sgn x) * (sgn (1 / x)) = 1 by Th18; :: thesis: verum