let a, b be Real; :: thesis: [\(a + b)/] = ([\a/] + [\b/]) + [\((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) + ((frac a) + (frac b)))/]
.= (k + l) + [\((frac a) + (frac b))/] by INT_1:28 ;
hence [\(a + b)/] = ([\a/] + [\b/]) + [\((frac a) + (frac b))/] ; :: thesis: verum