let n be Nat; :: thesis: for r being Real holds (rfs r) . (n + 1) = (rfs (1 / (frac r))) . n
let r be Real; :: 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 Lm6; :: thesis: verum