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