let x0, x1 be Real; :: thesis: ( x0 in dom tan & x1 in dom tan implies [!tan ,x0,x1!] = (sin (x0 - x1)) / (((cos x0) * (cos x1)) * (x0 - x1)) )
assume A1: ( x0 in dom tan & x1 in dom tan ) ; :: thesis: [!tan ,x0,x1!] = (sin (x0 - x1)) / (((cos x0) * (cos x1)) * (x0 - x1))
then A2: ( cos x0 <> 0 & cos x1 <> 0 ) by FDIFF_8:1;
A3: tan . x0 = (sin . x0) * ((cos . x0) " ) by A1, RFUNCT_1:def 4
.= (sin . x0) * (1 / (cos . x0)) by XCMPLX_1:217
.= tan x0 by XCMPLX_1:100 ;
tan . x1 = (sin . x1) * ((cos . x1) " ) by A1, RFUNCT_1:def 4
.= (sin . x1) * (1 / (cos . x1)) by XCMPLX_1:217
.= tan x1 by XCMPLX_1:100 ;
then [!tan ,x0,x1!] = ((sin (x0 - x1)) / ((cos x0) * (cos x1))) / (x0 - x1) by A2, A3, SIN_COS4:24
.= (sin (x0 - x1)) / (((cos x0) * (cos x1)) * (x0 - x1)) by XCMPLX_1:79 ;
hence [!tan ,x0,x1!] = (sin (x0 - x1)) / (((cos x0) * (cos x1)) * (x0 - x1)) ; :: thesis: verum