theorem FR2: :: NEWTON06:14

for a, b being Real holds frac (a * b) = frac ((([\a/] * (frac b)) + ([\b/] * (frac a))) + ((frac a) * (frac b)))