let x be Real; :: thesis: x = |.x.| * (sgn x)
A1: ( 0 < x implies x = |.x.| * (sgn x) )

proof

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

end;

A3: ( x < 0 implies x = |.x.| * (sgn x) )

proof

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

end;

( x = 0 implies x = |.x.| * (sgn x) ) ;
hence x = |.x.| * (sgn x) by A1, A3; :: thesis: verum