theorem :: NUMERAL3:4

for r being Real holds [\|.r.|/] + (frac |.r.|) = r * (sgn r)