theorem Th73: :: REAL_3:73

for r being Real st ( for n being Nat holds (scf r) . n > 0 ) holds
(cocf r) . 2 = ((scf r) . 0) + (1 / (((scf r) . 1) + (1 / ((scf r) . 2))))