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