let x be real number ; :: thesis: sgn (sgn x) = sgn x
A1: ( 0 < x or x < 0 or x = 0 ) ;
A2: ( 0 < x implies sgn (sgn x) = sgn x )

proof

assume A3: 0 < x ; :: thesis: sgn (sgn x) = sgn x
then sgn (sgn x) = sgn 1 by Def2
.= 1 by Def2 ;
hence sgn (sgn x) = sgn x by A3, Def2; :: thesis: verum

end;

( x < 0 implies sgn (sgn x) = sgn x )

proof

assume A4: x < 0 ; :: thesis: sgn (sgn x) = sgn x
then sgn (sgn x) = sgn (- 1) by Def2
.= - 1 by Def2 ;
hence sgn (sgn x) = sgn x by A4, Def2; :: thesis: verum

end;

hence sgn (sgn x) = sgn x by A1, A2, Def2; :: thesis: verum