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