let r be real number ; :: thesis: frac r = r - ((scf r) . 0)
thus frac r = r - [\((rfs r) . 0)/] by Def4
.= r - ((scf r) . 0) by Def5 ; :: thesis: verum