let x0, x1 be Real; :: thesis: ( x0 in dom tan & x1 in dom tan implies [!((tan (#) tan) (#) cos),x0,x1!] = [!(tan (#) sin),x0,x1!] )
assume A1: ( x0 in dom tan & x1 in dom tan ) ; :: thesis: [!((tan (#) tan) (#) cos),x0,x1!] = [!(tan (#) sin),x0,x1!]
[!((tan (#) tan) (#) cos),x0,x1!] = ((((tan (#) tan) . x0) * (cos . x0)) - (((tan (#) tan) (#) cos) . x1)) / (x0 - x1) by VALUED_1:5
.= ((((tan . x0) * (tan . x0)) * (cos . x0)) - (((tan (#) tan) (#) cos) . x1)) / (x0 - x1) by VALUED_1:5
.= ((((tan . x0) * (tan . x0)) * (cos . x0)) - (((tan (#) tan) . x1) * (cos . x1))) / (x0 - x1) by VALUED_1:5
.= ((((tan . x0) * (tan . x0)) * (cos . x0)) - (((tan . x1) * (tan . x1)) * (cos . x1))) / (x0 - x1) by VALUED_1:5
.= (((((sin . x0) * ((cos . x0) ")) * (tan . x0)) * (cos . x0)) - (((tan . x1) * (tan . x1)) * (cos . x1))) / (x0 - x1) by A1, RFUNCT_1:def 1
.= (((((sin . x0) * ((cos . x0) ")) * (tan . x0)) * (cos . x0)) - ((((sin . x1) * ((cos . x1) ")) * (tan . x1)) * (cos . x1))) / (x0 - x1) by A1, RFUNCT_1:def 1
.= ((((sin . x0) * ((cos . x0) * (1 / (cos . x0)))) * (tan . x0)) - (((sin . x1) * ((cos . x1) * (1 / (cos . x1)))) * (tan . x1))) / (x0 - x1)
.= ((((sin . x0) * 1) * (tan . x0)) - (((sin . x1) * ((cos . x1) * (1 / (cos . x1)))) * (tan . x1))) / (x0 - x1) by A1, FDIFF_8:1, XCMPLX_1:106
.= ((((sin . x0) * 1) * (tan . x0)) - (((sin . x1) * 1) * (tan . x1))) / (x0 - x1) by A1, FDIFF_8:1, XCMPLX_1:106
.= (((tan (#) sin) . x0) - ((tan . x1) * (sin . x1))) / (x0 - x1) by VALUED_1:5
.= [!(tan (#) sin),x0,x1!] by VALUED_1:5 ;
hence [!((tan (#) tan) (#) cos),x0,x1!] = [!(tan (#) sin),x0,x1!] ; :: thesis: verum