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