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 <= [/r\] & [/r\] < r + 1 ) by Def5;
then [/r\] + i0 < (r + 1) + i0 by XREAL_1:8;
then A2: [/r\] + i0 < (r + i0) + 1 ;
r + i0 <= [/r\] + i0 by A1, XREAL_1:8;
hence [/r\] + i0 = [/(r + i0)\] by A2, Def5; :: thesis: verum