theorem :: REAL_3:36

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