let a, b be Real; :: thesis: frac (a * b) = frac (((a * (frac b)) + (b * (frac a))) - ((frac a) * (frac b)))
( a = [\a/] + (frac a) & b = [\b/] + (frac b) ) by INT_1:42;
then frac (a * b) = frac (([\a/] * [\b/]) + (((a * (frac b)) + (b * (frac a))) - ((frac a) * (frac b))))
.= frac (((a * (frac b)) + (b * (frac a))) - ((frac a) * (frac b))) by INT_1:66 ;
hence frac (a * b) = frac (((a * (frac b)) + (b * (frac a))) - ((frac a) * (frac b))) ; :: thesis: verum