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