let a be Integer; :: thesis: for b being non zero Integer holds frac (b * (frac (a / b))) = 0
let b be non zero Integer; :: thesis: frac (b * (frac (a / b))) = 0
frac (b * (frac (a / b))) = frac (b * (a / b)) by FR3
.= frac a by XCMPLX_1:87 ;
hence frac (b * (frac (a / b))) = 0 ; :: thesis: verum