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