theorem :: REALALG3:30

for R being ordered domRing
for P being Ordering of R
for a being Element of R holds a = (signum (P,a)) '*' (abs (P,a))