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