let i be Integer; :: thesis: for r being Real holds frac (r + i) = frac r
let r be Real; :: thesis: frac (r + i) = frac r
thus frac (r + i) = (r + i) - [\(r + i)/]
.= (r + i) - ([\r/] + i) by Th28
.= ((r - [\r/]) + i) - i
.= frac r ; :: thesis: verum