let r be Real; ( ( for n being Nat holds (scf r) . n > 0 ) implies (cocf r) . 2 = ((scf r) . 0) + (1 / (((scf r) . 1) + (1 / ((scf r) . 2)))) )
set s = scf r;
A1: (cocf r) . 2 =
((c_n r) . 2) * (((c_d r) ") . 2)
by SEQ_1:8
.=
((c_n r) . 2) * (((c_d r) . 2) ")
by VALUED_1:10
.=
((c_n r) . 2) * (1 / ((c_d r) . 2))
.=
((c_n r) . 2) / ((c_d r) . 2)
;
assume A2:
for n being Nat holds (scf r) . n > 0
; (cocf r) . 2 = ((scf r) . 0) + (1 / (((scf r) . 1) + (1 / ((scf r) . 2))))
then A3:
(scf r) . 1 > 0
;
A4: (c_d r) . 2 =
(((scf r) . (0 + 2)) * ((c_d r) . (0 + 1))) + ((c_d r) . 0)
by Def6
.=
(((scf r) . 2) * ((scf r) . 1)) + ((c_d r) . 0)
by Def6
.=
(((scf r) . 2) * ((scf r) . 1)) + 1
by Def6
;
A5: (c_n r) . 2 =
(((scf r) . (0 + 2)) * ((c_n r) . (0 + 1))) + ((c_n r) . 0)
by Def5
.=
(((scf r) . 2) * ((((scf r) . 1) * ((scf r) . 0)) + 1)) + ((c_n r) . 0)
by Def5
.=
(((((scf r) . 2) * ((scf r) . 1)) * ((scf r) . 0)) + ((scf r) . 2)) + ((scf r) . 0)
by Def5
;
A6:
(scf r) . 2 > 0
by A2;
then ((scf r) . 0) + (1 / (((scf r) . 1) + (1 / ((scf r) . 2)))) =
((scf r) . 0) + (1 / (((((scf r) . 1) * ((scf r) . 2)) + 1) / ((scf r) . 2)))
by XCMPLX_1:113
.=
((scf r) . 0) + (((scf r) . 2) / ((((scf r) . 1) * ((scf r) . 2)) + 1))
by XCMPLX_1:57
.=
((((scf r) . 0) * ((((scf r) . 1) * ((scf r) . 2)) + 1)) + ((scf r) . 2)) / ((((scf r) . 1) * ((scf r) . 2)) + 1)
by A3, A6, XCMPLX_1:113
.=
(cocf r) . 2
by A1, A5, A4
;
hence
(cocf r) . 2 = ((scf r) . 0) + (1 / (((scf r) . 1) + (1 / ((scf r) . 2))))
; verum