let r be real number ; :: thesis: for i0 being Integer holds [\r/] + i0 = [\(r + i0)/]
let i0 be Integer; :: thesis: [\r/] + i0 = [\(r + i0)/]
A1: ( r - 1 < [\r/] & [\r/] <= r ) by Def4;
then (r - 1) + i0 < [\r/] + i0 by XREAL_1:8;
then A2: (r + i0) - 1 < [\r/] + i0 ;
[\r/] + i0 <= r + i0 by A1, XREAL_1:8;
hence [\r/] + i0 = [\(r + i0)/] by A2, Def4; :: thesis: verum