signum . 0 = sgn 0 by Def9
.= 0 by ABSVALUE:def 2 ;
hence signum . 0 = 0 ; :: thesis: verum