let x0, x1 be Real; ( 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 )
; [!((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!]
; verum