let n be Nat; :: thesis: for r being Real holds (rfs r) . (n + 1) = 1 / (((rfs r) . n) - ((scf r) . n))
let r be Real; :: thesis: (rfs r) . (n + 1) = 1 / (((rfs r) . n) - ((scf r) . n))
thus (rfs r) . (n + 1) = 1 / (frac ((rfs r) . n)) by Def3
.= 1 / (((rfs r) . n) - ((scf r) . n)) by Def4 ; :: thesis: verum