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