for r being Real holds (cocf r) . 0 = (scf r) . 0