let x be Real; :: thesis: 1 / (sgn x) = sgn (1 / x)

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

suppose A1: x = 0 ; :: thesis: 1 / (sgn x) = sgn (1 / x)

hence 1 / (sgn x) = 1 / 0 by Def2
.= sgn (1 / x) by A1, Def2 ;
:: thesis: verum

end;

suppose A2: x <> 0 ; :: thesis: 1 / (sgn x) = sgn (1 / x)

then ((sgn x) * (sgn (1 / x))) * (1 / (sgn x)) = 1 * (1 / (sgn x)) by Th20;
then (sgn (1 / x)) * ((sgn x) * (1 / (sgn x))) = 1 / (sgn x) ;
then (sgn (1 / x)) * 1 = 1 / (sgn x) by A2, Th16, XCMPLX_1:106;
hence 1 / (sgn x) = sgn (1 / x) ; :: thesis: verum

end;

end;