let n be Nat; :: thesis: for r being real number holds (rfs r) . (n + 1) = (rfs (1 / (frac r))) . n
let r be real number ; :: thesis: (rfs r) . (n + 1) = (rfs (1 / (frac r))) . n
frac r = r - ((scf r) . 0) by Th35;
hence (rfs r) . (n + 1) = (rfs (1 / (frac r))) . n by Lm8; :: thesis: verum