let x0, x1 be Real; ( x0 in dom tan & x1 in dom tan implies [!((tan (#) tan) (#) sin),x0,x1!] = ((((sin x0) |^ 3) * ((cos x1) ^2)) - (((sin x1) |^ 3) * ((cos x0) ^2))) / ((((cos x0) ^2) * ((cos x1) ^2)) * (x0 - x1)) )
assume A1:
( x0 in dom tan & x1 in dom tan )
; [!((tan (#) tan) (#) sin),x0,x1!] = ((((sin x0) |^ 3) * ((cos x1) ^2)) - (((sin x1) |^ 3) * ((cos x0) ^2))) / ((((cos x0) ^2) * ((cos x1) ^2)) * (x0 - x1))
A2:
( cos x0 <> 0 & cos x1 <> 0 )
by A1, FDIFF_8:1;
[!((tan (#) tan) (#) sin),x0,x1!] =
((((tan (#) tan) . x0) * (sin . x0)) - (((tan (#) tan) (#) sin) . x1)) / (x0 - x1)
by VALUED_1:5
.=
((((tan . x0) * (tan . x0)) * (sin . x0)) - (((tan (#) tan) (#) sin) . x1)) / (x0 - x1)
by VALUED_1:5
.=
((((tan . x0) * (tan . x0)) * (sin . x0)) - (((tan (#) tan) . x1) * (sin . x1))) / (x0 - x1)
by VALUED_1:5
.=
((((tan . x0) * (tan . x0)) * (sin . x0)) - (((tan . x1) * (tan . x1)) * (sin . x1))) / (x0 - x1)
by VALUED_1:5
.=
(((((sin . x0) * ((cos . x0) ")) * (tan . x0)) * (sin . x0)) - (((tan . x1) * (tan . x1)) * (sin . x1))) / (x0 - x1)
by A1, RFUNCT_1:def 1
.=
(((((sin . x0) * ((cos . x0) ")) * ((sin . x0) * ((cos . x0) "))) * (sin . x0)) - (((tan . x1) * (tan . x1)) * (sin . x1))) / (x0 - x1)
by A1, RFUNCT_1:def 1
.=
(((((sin . x0) * ((cos . x0) ")) * ((sin . x0) * ((cos . x0) "))) * (sin . x0)) - ((((sin . x1) * ((cos . x1) ")) * (tan . x1)) * (sin . x1))) / (x0 - x1)
by A1, RFUNCT_1:def 1
.=
(((((sin . x0) * ((cos . x0) ")) * ((sin . x0) * ((cos . x0) "))) * (sin . x0)) - ((((sin . x1) * ((cos . x1) ")) * ((sin . x1) * ((cos . x1) "))) * (sin . x1))) / (x0 - x1)
by A1, RFUNCT_1:def 1
.=
((((((sin . x0) * (sin . x0)) * (sin . x0)) * ((cos . x0) ")) * ((cos . x0) ")) - (((((sin . x1) * (sin . x1)) * (sin . x1)) * ((cos . x1) ")) * ((cos . x1) "))) / (x0 - x1)
.=
(((((((sin . x0) |^ 1) * (sin . x0)) * (sin . x0)) * ((cos . x0) ")) * ((cos . x0) ")) - (((((sin . x1) * (sin . x1)) * (sin . x1)) * ((cos . x1) ")) * ((cos . x1) "))) / (x0 - x1)
.=
((((((sin . x0) |^ (1 + 1)) * (sin . x0)) * ((cos . x0) ")) * ((cos . x0) ")) - (((((sin . x1) * (sin . x1)) * (sin . x1)) * ((cos . x1) ")) * ((cos . x1) "))) / (x0 - x1)
by NEWTON:6
.=
(((((sin . x0) |^ (2 + 1)) * ((cos . x0) ")) * ((cos . x0) ")) - (((((sin . x1) * (sin . x1)) * (sin . x1)) * ((cos . x1) ")) * ((cos . x1) "))) / (x0 - x1)
by NEWTON:6
.=
(((((sin . x0) |^ 3) * ((cos . x0) ")) * ((cos . x0) ")) - ((((((sin . x1) |^ 1) * (sin . x1)) * (sin . x1)) * ((cos . x1) ")) * ((cos . x1) "))) / (x0 - x1)
.=
(((((sin . x0) |^ 3) * ((cos . x0) ")) * ((cos . x0) ")) - (((((sin . x1) |^ (1 + 1)) * (sin . x1)) * ((cos . x1) ")) * ((cos . x1) "))) / (x0 - x1)
by NEWTON:6
.=
(((((sin . x0) |^ 3) * ((cos . x0) ")) * ((cos . x0) ")) - ((((sin . x1) |^ (2 + 1)) * ((cos . x1) ")) * ((cos . x1) "))) / (x0 - x1)
by NEWTON:6
.=
((((sin . x0) |^ 3) * (((cos . x0) ") * ((cos . x0) "))) - ((((sin . x1) |^ 3) * ((cos . x1) ")) * ((cos . x1) "))) / (x0 - x1)
.=
((((sin . x0) |^ 3) * (((cos . x0) * (cos . x0)) ")) - (((sin . x1) |^ 3) * (((cos . x1) ") * ((cos . x1) ")))) / (x0 - x1)
by XCMPLX_1:204
.=
((((sin . x0) |^ 3) / ((cos . x0) ^2)) - (((sin . x1) |^ 3) / ((cos . x1) ^2))) / (x0 - x1)
by XCMPLX_1:204
.=
(((((sin x0) |^ 3) * ((cos x1) ^2)) - (((sin x1) |^ 3) * ((cos x0) ^2))) / (((cos x0) ^2) * ((cos x1) ^2))) / (x0 - x1)
by A2, XCMPLX_1:130
.=
((((sin x0) |^ 3) * ((cos x1) ^2)) - (((sin x1) |^ 3) * ((cos x0) ^2))) / ((((cos x0) ^2) * ((cos x1) ^2)) * (x0 - x1))
by XCMPLX_1:78
;
hence
[!((tan (#) tan) (#) sin),x0,x1!] = ((((sin x0) |^ 3) * ((cos x1) ^2)) - (((sin x1) |^ 3) * ((cos x0) ^2))) / ((((cos x0) ^2) * ((cos x1) ^2)) * (x0 - x1))
; verum