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