let r be real number ; ( (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:12
.=
((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 Def6
.=
((((scf r) . 1) * ((scf r) . 0 )) + 1) / ((scf r) . 1)
by Def7
.=
((scf r) . 0 ) + (1 / ((scf r) . 1))
by A1, XCMPLX_1:114
; verum