theorem Th37: :: REAL_3:37

for n being Nat
for r being Real holds (scf r) . (n + 1) = (scf (1 / (frac r))) . n