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 that
A1: x0 in dom sec and
A2: x1 in dom sec ; :: thesis: [!sec,x0,x1!] = - (((2 * (sin ((x1 + x0) / 2))) * (sin ((x1 - x0) / 2))) / (((cos x1) * (cos x0)) * (x0 - x1)))
A3: sec . x1 = (cos . x1) " by A2, RFUNCT_1:def 2
.= sec x1 by XCMPLX_1:215 ;
sec . x0 = (cos . x0) " by A1, RFUNCT_1:def 2
.= sec x0 by XCMPLX_1:215 ;
then [!sec,x0,x1!] = (((1 * (cos x1)) / ((cos x0) * (cos x1))) - (1 / (cos x1))) / (x0 - x1) by A2, A3, RFUNCT_1:3, XCMPLX_1:91
.= (((1 * (cos x1)) / ((cos x0) * (cos x1))) - ((1 * (cos x0)) / ((cos x1) * (cos x0)))) / (x0 - x1) by A1, RFUNCT_1:3, XCMPLX_1:91
.= (((cos x1) - (cos x0)) / ((cos x1) * (cos x0))) / (x0 - x1) by XCMPLX_1:120
.= ((cos x1) - (cos x0)) / (((cos x1) * (cos x0)) * (x0 - x1)) by XCMPLX_1:78
.= (- (2 * ((sin ((x1 + x0) / 2)) * (sin ((x1 - x0) / 2))))) / (((cos x1) * (cos x0)) * (x0 - x1)) by SIN_COS4:18
.= - ((2 * ((sin ((x1 + x0) / 2)) * (sin ((x1 - x0) / 2)))) / (((cos x1) * (cos x0)) * (x0 - x1))) by XCMPLX_1:187 ;
hence [!sec,x0,x1!] = - (((2 * (sin ((x1 + x0) / 2))) * (sin ((x1 - x0) / 2))) / (((cos x1) * (cos x0)) * (x0 - x1))) ; :: thesis: verum