let r be real number ; :: thesis: (cocf r) . 0 = (scf r) . 0
thus (cocf r) . 0 = ((c_n r) . 0 ) * (((c_d r) " ) . 0 ) by SEQ_1:12
.= ((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 Def6
.= ((scf r) . 0 ) / 1 by Def7
.= (scf r) . 0 ; :: thesis: verum