let
x
be
Real
;
:: thesis:
(
x
>
0
implies
signum
.
x
=
1 )
assume
A1
:
0
<
x
;
:: thesis:
signum
.
x
=
1
signum
.
x
=
sgn
x
by
Def9
.= 1
by
A1
,
ABSVALUE:def 2
;
hence
signum
.
x
=
1 ;
:: thesis:
verum