theorem Th1: :: DIOPHAN1:1

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