theorem :: ABSVALUE:17

for x being Real holds x = |.x.| * (sgn x)