let r be Real; :: thesis: for i0 being Integer holds [\r/] + i0 = [\(r + i0)/]
let i0 be Integer; :: thesis: [\r/] + i0 = [\(r + i0)/]
r - 1 < [\r/] by Def6;
then (r - 1) + i0 < [\r/] + i0 by XREAL_1:6;
then A1: (r + i0) - 1 < [\r/] + i0 ;
[\r/] <= r by Def6;
then [\r/] + i0 <= r + i0 by XREAL_1:6;
hence [\r/] + i0 = [\(r + i0)/] by A1, Def6; :: thesis: verum