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 that
A1: x0 in dom tan and
A2: x1 in dom tan ; :: thesis: [!tan,x0,x1!] = (sin (x0 - x1)) / (((cos x0) * (cos x1)) * (x0 - x1))
A3: tan . x0 = (sin . x0) * ((cos . x0) ") by A1, RFUNCT_1:def 1
.= (sin . x0) * (1 / (cos . x0)) by XCMPLX_1:215
.= tan x0 by XCMPLX_1:99 ;
A4: tan . x1 = (sin . x1) * ((cos . x1) ") by A2, RFUNCT_1:def 1
.= (sin . x1) * (1 / (cos . x1)) by XCMPLX_1:215
.= tan x1 by XCMPLX_1:99 ;
( cos x0 <> 0 & cos x1 <> 0 ) by A1, A2, FDIFF_8:1;
then [!tan,x0,x1!] = ((sin (x0 - x1)) / ((cos x0) * (cos x1))) / (x0 - x1) by A3, A4, SIN_COS4:20
.= (sin (x0 - x1)) / (((cos x0) * (cos x1)) * (x0 - x1)) by XCMPLX_1:78 ;
hence [!tan,x0,x1!] = (sin (x0 - x1)) / (((cos x0) * (cos x1)) * (x0 - x1)) ; :: thesis: verum