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)/]
.= (r + i) - ([\r/] + i) by Th51
.= ((r - [\r/]) + i) - i
.= frac r ; :: thesis: verum