:: deftheorem sgnF defines signum REALALG3:def 10 :
for R being ordered Ring
for P being Ordering of R
for b₃ being Function of the carrier of R,INT holds
( b₃ = signum P iff for a being Element of R holds b₃ . a = signum (P,a) );