theorem A17: :: NUMERAL3:3

for r being Real holds
( r * (sgn r) = |.r.| & r / (sgn r) = |.r.| & r = |.r.| / (sgn r) )