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

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

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

hence sgn (x / y) = sgn (x * (0 ")) by XCMPLX_0:def 9
.= (sgn x) * (0 ") by Def2
.= (sgn x) / 0 by XCMPLX_0:def 9
.= (sgn x) / (sgn y) by A1, Def2 ;
:: thesis: verum

end;

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

x / y = (x / y) * 1
.= (x / y) * (y * (1 / y)) by A2, XCMPLX_1:106
.= ((x / y) * y) * (1 / y)
.= x * (1 / y) by A2, XCMPLX_1:87 ;
then sgn (x / y) = (sgn x) * (sgn (1 / y)) by Th18
.= ((sgn x) / 1) * (1 / (sgn y)) by Th21
.= ((sgn x) * 1) / (1 * (sgn y)) by XCMPLX_1:76
.= (sgn x) / (1 * (sgn y)) ;
hence sgn (x / y) = (sgn x) / (sgn y) ; :: thesis: verum

end;

end;