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