let d be Real; :: thesis: |.(sgn d).| <= 1

per cases ( d > 0 or d < 0 or d = 0 ) ;

suppose d > 0 ; :: thesis: |.(sgn d).| <= 1

then sgn d = 1 by ABSVALUE:def 2;
hence |.(sgn d).| <= 1 ; :: thesis: verum

end;

suppose d < 0 ; :: thesis: |.(sgn d).| <= 1

then sgn d = - 1 by ABSVALUE:def 2;
then |.(sgn d).| = - (- 1) by ABSVALUE:def 1
.= 1 ;
hence |.(sgn d).| <= 1 ; :: thesis: verum

end;

suppose d = 0 ; :: thesis: |.(sgn d).| <= 1

then sgn d = 0 by ABSVALUE:def 2;
hence |.(sgn d).| <= 1 ; :: thesis: verum

end;

end;