let h, x be Real; ( x in dom tan & x + h in dom tan implies (fD (((tan (#) tan) (#) cos),h)) . x = ((tan (#) sin) . (x + h)) - ((tan (#) sin) . x) )
set f = (tan (#) tan) (#) cos;
assume A1:
( x in dom tan & x + h in dom tan )
; (fD (((tan (#) tan) (#) cos),h)) . x = ((tan (#) sin) . (x + h)) - ((tan (#) sin) . x)
( x in dom ((tan (#) tan) (#) cos) & x + h in dom ((tan (#) tan) (#) cos) )
then (fD (((tan (#) tan) (#) cos),h)) . x =
(((tan (#) tan) (#) cos) . (x + h)) - (((tan (#) tan) (#) cos) . x)
by DIFF_1:1
.=
(((tan (#) tan) . (x + h)) * (cos . (x + h))) - (((tan (#) tan) (#) cos) . x)
by VALUED_1:5
.=
(((tan . (x + h)) * (tan . (x + h))) * (cos . (x + h))) - (((tan (#) tan) (#) cos) . x)
by VALUED_1:5
.=
(((tan . (x + h)) * (tan . (x + h))) * (cos . (x + h))) - (((tan (#) tan) . x) * (cos . x))
by VALUED_1:5
.=
(((tan . (x + h)) * (tan . (x + h))) * (cos . (x + h))) - (((tan . x) * (tan . x)) * (cos . x))
by VALUED_1:5
.=
((((sin . (x + h)) * ((cos . (x + h)) ")) * (tan . (x + h))) * (cos . (x + h))) - (((tan . x) * (tan . x)) * (cos . x))
by A1, RFUNCT_1:def 1
.=
((((sin . (x + h)) * ((cos . (x + h)) ")) * (tan . (x + h))) * (cos . (x + h))) - ((((sin . x) * ((cos . x) ")) * (tan . x)) * (cos . x))
by A1, RFUNCT_1:def 1
.=
(((sin . (x + h)) * (tan . (x + h))) * ((cos . (x + h)) * (1 / (cos . (x + h))))) - (((sin . x) * (tan . x)) * ((cos . x) * (1 / (cos . x))))
.=
(((sin . (x + h)) * (tan . (x + h))) * 1) - (((sin . x) * (tan . x)) * ((cos . x) * (1 / (cos . x))))
by A1, FDIFF_8:1, XCMPLX_1:106
.=
(((sin . (x + h)) * (tan . (x + h))) * 1) - (((sin . x) * (tan . x)) * 1)
by A1, FDIFF_8:1, XCMPLX_1:106
.=
((tan (#) sin) . (x + h)) - ((tan . x) * (sin . x))
by VALUED_1:5
.=
((tan (#) sin) . (x + h)) - ((tan (#) sin) . x)
by VALUED_1:5
;
hence
(fD (((tan (#) tan) (#) cos),h)) . x = ((tan (#) sin) . (x + h)) - ((tan (#) sin) . x)
; verum