theorem Th26: :: REAL_3:26

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