theorem FR3: :: NEWTON06:15

for a being Real
for b being Integer holds frac (a * b) = frac (b * (frac a))