theorem FR1: :: NEWTON06:13

for a, b being Real holds frac (a * b) = frac (((a * (frac b)) + (b * (frac a))) - ((frac a) * (frac b)))