theorem Th72: :: REAL_3:72

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