let a, b be Real; :: thesis: [\(a * b)/] = ([\a/] * [\b/]) + [\((([\a/] * (frac b)) + ([\b/] * (frac a))) + ((frac a) * (frac b)))/]
reconsider k = [\a/], l = [\b/] as Integer ;
( a = k + (frac a) & b = l + (frac b) ) by INT_1:42;
then [\(a * b)/] = [\((k * l) + (((k * (frac b)) + (l * (frac a))) + ((frac a) * (frac b))))/]
.= (k * l) + [\(((k * (frac b)) + (l * (frac a))) + ((frac a) * (frac b)))/] by INT_1:28 ;
hence [\(a * b)/] = ([\a/] * [\b/]) + [\((([\a/] * (frac b)) + ([\b/] * (frac a))) + ((frac a) * (frac b)))/] ; :: thesis: verum