let i be Integer; :: thesis: for r being real number holds frac (r + i) = frac r
let r be real number ; :: thesis: frac (r + i) = frac r
thus frac (r + i) = (r + i) - [\(r + i)/] by INT_1:def 6
.= (r + i) - ([\r/] + i) by INT_1:51
.= ((r - [\r/]) + i) - i
.= frac r by INT_1:def 6 ; :: thesis: verum