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