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

proof

assume A2: 0 < x ; :: thesis: x = (abs x) * (sgn x)
then abs x = x by Def1;
then (abs x) * (sgn x) = x * 1 by A2, Def2;
hence x = (abs x) * (sgn x) ; :: thesis: verum

end;

A3: ( x < 0 implies x = (abs x) * (sgn x) )

proof

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

end;

( x = 0 implies x = (abs x) * (sgn x) )

proof

assume A5: x = 0 ; :: thesis: x = (abs x) * (sgn x)
then sgn x = 0 by Def2;
hence x = (abs x) * (sgn x) by A5; :: thesis: verum

end;

hence x = (abs x) * (sgn x) by A1, A3; :: thesis: verum