let r be real number ; :: thesis:
set s = scf r;
assume A1: for n being Nat holds (scf r) . n > 0 ; :: thesis:
then A2: ( (scf r) . 1 > 0 & (scf r) . 2 > 0 & (scf r) . 3 > 0 ) ;
then ((scf r) . 2) * ((scf r) . 3) > 0 by XREAL_1:131;
then A3: (((scf r) . 2) * ((scf r) . 3)) + 1 > 0 ;
((scf r) . 1) * ((((scf r) . 2) * ((scf r) . 3)) + 1) > 0 by A2, XREAL_1:131;
then A4: (((scf r) . 1) * ((((scf r) . 2) * ((scf r) . 3)) + 1)) + ((scf r) . 3) > 0 by A1, XREAL_1:36;
A5: (cocf r) . 3 = ((c_n r) . 3) * (((c_d r) " ) . 3) by SEQ_1:12
.= ((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) ;
A6: (c_n r) . 2 = (((scf r) . (0 + 2)) * ((c_n r) . (0 + 1))) + ((c_n r) . 0 ) by Def6
.= (((scf r) . 2) * ((((scf r) . 1) * ((scf r) . 0 )) + 1)) + ((c_n r) . 0 ) by Def6
.= (((((scf r) . 2) * ((scf r) . 1)) * ((scf r) . 0 )) + ((scf r) . 2)) + ((scf r) . 0 ) by Def6 ;
A7: (c_n r) . 3 = (((scf r) . (1 + 2)) * ((c_n r) . (1 + 1))) + ((c_n r) . 1) by Def6
.= (((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, Def6
.= ((((((((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: (c_d r) . 2 = (((scf r) . (0 + 2)) * ((c_d r) . (0 + 1))) + ((c_d r) . 0 ) by Def7
.= (((scf r) . 2) * ((scf r) . 1)) + ((c_d r) . 0 ) by Def7
.= (((scf r) . 2) * ((scf r) . 1)) + 1 by Def7 ;
A9: (c_d r) . 3 = (((scf r) . (1 + 2)) * ((c_d r) . (1 + 1))) + ((c_d r) . 1) by Def7
.= (((scf r) . 3) * ((((scf r) . 2) * ((scf r) . 1)) + 1)) + ((scf r) . 1) by A8, Def7
.= (((scf r) . 1) * ((((scf r) . 2) * ((scf r) . 3)) + 1)) + ((scf r) . 3) ;
((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 A2, XCMPLX_1:114
.= ((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 A3, XCMPLX_1:114
.= ((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 A4, XCMPLX_1:114 ;
hence (cocf r) . 3 = ((scf r) . 0 ) + (1 / (((scf r) . 1) + (1 / (((scf r) . 2) + (1 / ((scf r) . 3)))))) by A5, A7, A9; :: thesis: