theorem Th35: :: REAL_3:35

for r being Real holds frac r = r - ((scf r) . 0)