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 Def4
.= 1 by ABSVALUE:def 2, A1 ;
hence signum . x = 1 ; :: thesis: verum