let x be real number ; :: thesis: ( x < 0 implies signum . x = - 1 )
assume A1: 0 > x ; :: thesis: signum . x = - 1
x in REAL by XREAL_0:def 1;
then signum . x = sgn x by Def9
.= - 1 by A1, ABSVALUE:def 2 ;
hence signum . x = - 1 ; :: thesis: verum