let r be Real; ( (scf r) . 1 <> 0 implies (cocf r) . 1 = ((scf r) . 0) + (1 / ((scf r) . 1)) )
set s = scf r;
assume A1:
(scf r) . 1 <> 0
; (cocf r) . 1 = ((scf r) . 0) + (1 / ((scf r) . 1))
thus (cocf r) . 1 =
((c_n r) . 1) * (((c_d r) ") . 1)
by SEQ_1:8
.=
((c_n r) . 1) * (((c_d r) . 1) ")
by VALUED_1:10
.=
((c_n r) . 1) * (1 / ((c_d r) . 1))
.=
((c_n r) . 1) / ((c_d r) . 1)
.=
((((scf r) . 1) * ((scf r) . 0)) + 1) / ((c_d r) . 1)
by Def5
.=
((((scf r) . 1) * ((scf r) . 0)) + 1) / ((scf r) . 1)
by Def6
.=
((scf r) . 0) + (1 / ((scf r) . 1))
by A1, XCMPLX_1:113
; verum