let x0, x1 be Real; :: thesis: ( x0 in dom sec & x1 in dom sec implies [!sec ,x0,x1!] = - (((2 * (sin ((x1 + x0) / 2))) * (sin ((x1 - x0) / 2))) / (((cos x1) * (cos x0)) * (x0 - x1))) )
assume A1: ( x0 in dom sec & x1 in dom sec ) ; :: thesis: [!sec ,x0,x1!] = - (((2 * (sin ((x1 + x0) / 2))) * (sin ((x1 - x0) / 2))) / (((cos x1) * (cos x0)) * (x0 - x1)))
then A2: sec . x0 = (cos . x0) " by RFUNCT_1:def 8
.= sec x0 by XCMPLX_1:217 ;
sec . x1 = (cos . x1) " by A1, RFUNCT_1:def 8
.= sec x1 by XCMPLX_1:217 ;
then [!sec ,x0,x1!] = (((1 * (cos x1)) / ((cos x0) * (cos x1))) - (1 / (cos x1))) / (x0 - x1) by A1, A2, RFUNCT_1:13, XCMPLX_1:92
.= (((1 * (cos x1)) / ((cos x0) * (cos x1))) - ((1 * (cos x0)) / ((cos x1) * (cos x0)))) / (x0 - x1) by A1, RFUNCT_1:13, XCMPLX_1:92
.= (((cos x1) - (cos x0)) / ((cos x1) * (cos x0))) / (x0 - x1) by XCMPLX_1:121
.= ((cos x1) - (cos x0)) / (((cos x1) * (cos x0)) * (x0 - x1)) by XCMPLX_1:79
.= (- (2 * ((sin ((x1 + x0) / 2)) * (sin ((x1 - x0) / 2))))) / (((cos x1) * (cos x0)) * (x0 - x1)) by SIN_COS4:22
.= - ((2 * ((sin ((x1 + x0) / 2)) * (sin ((x1 - x0) / 2)))) / (((cos x1) * (cos x0)) * (x0 - x1))) by XCMPLX_1:188 ;
hence [!sec ,x0,x1!] = - (((2 * (sin ((x1 + x0) / 2))) * (sin ((x1 - x0) / 2))) / (((cos x1) * (cos x0)) * (x0 - x1))) ; :: thesis: verum