:: deftheorem Def9 defines signum FUNCT_8:def 9 :
for b₁ being Function of REAL,REAL holds
( b₁ = signum iff for x being Real holds b₁ . x = sgn x );