let r be Real; :: thesis: (cocf r) . 0 = (scf r) . 0
thus (cocf r) . 0 = ((c_n r) . 0) * (((c_d r) ") . 0) by SEQ_1:8
.= ((c_n r) . 0) * (((c_d r) . 0) ") by VALUED_1:10
.= ((c_n r) . 0) * (1 / ((c_d r) . 0))
.= ((c_n r) . 0) / ((c_d r) . 0)
.= ((scf r) . 0) / ((c_d r) . 0) by Def5
.= ((scf r) . 0) / 1 by Def6
.= (scf r) . 0 ; :: thesis: verum