let h, x be Real; ( x in dom cot & x + h in dom cot implies (fD ((cot (#) cot),h)) . x = ((1 / 2) * ((cos (2 * (x + h))) - (cos (2 * x)))) / (((sin (x + h)) * (sin x)) ^2) )
set f = cot (#) cot;
assume A1:
( x in dom cot & x + h in dom cot )
; (fD ((cot (#) cot),h)) . x = ((1 / 2) * ((cos (2 * (x + h))) - (cos (2 * x)))) / (((sin (x + h)) * (sin x)) ^2)
A2:
( sin x <> 0 & sin (x + h) <> 0 )
by A1, FDIFF_8:2;
( x in dom (cot (#) cot) & x + h in dom (cot (#) cot) )
then (fD ((cot (#) cot),h)) . x =
((cot (#) cot) . (x + h)) - ((cot (#) cot) . x)
by DIFF_1:1
.=
((cot . (x + h)) * (cot . (x + h))) - ((cot (#) cot) . x)
by VALUED_1:5
.=
((cot . (x + h)) * (cot . (x + h))) - ((cot . x) * (cot . x))
by VALUED_1:5
.=
(((cos . (x + h)) * ((sin . (x + h)) ")) * (cot . (x + h))) - ((cot . x) * (cot . x))
by A1, RFUNCT_1:def 1
.=
(((cos . (x + h)) * ((sin . (x + h)) ")) * ((cos . (x + h)) * ((sin . (x + h)) "))) - ((cot . x) * (cot . x))
by A1, RFUNCT_1:def 1
.=
(((cos . (x + h)) * ((sin . (x + h)) ")) * ((cos . (x + h)) * ((sin . (x + h)) "))) - (((cos . x) * ((sin . x) ")) * (cot . x))
by A1, RFUNCT_1:def 1
.=
((cot (x + h)) ^2) - ((cot x) ^2)
by A1, RFUNCT_1:def 1
.=
((cot (x + h)) - (cot x)) * ((cot (x + h)) + (cot x))
.=
(- ((sin ((x + h) - x)) / ((sin (x + h)) * (sin x)))) * ((cot (x + h)) + (cot x))
by A2, SIN_COS4:24
.=
(- ((sin ((x + h) - x)) / ((sin (x + h)) * (sin x)))) * ((sin ((x + h) + x)) / ((sin (x + h)) * (sin x)))
by A2, SIN_COS4:23
.=
- (((sin ((x + h) - x)) / ((sin (x + h)) * (sin x))) * ((sin ((x + h) + x)) / ((sin (x + h)) * (sin x))))
.=
- (((sin ((2 * x) + h)) * (sin h)) / (((sin (x + h)) * (sin x)) ^2))
by XCMPLX_1:76
.=
- ((- ((1 / 2) * ((cos (((2 * x) + h) + h)) - (cos (((2 * x) + h) - h))))) / (((sin (x + h)) * (sin x)) ^2))
by SIN_COS4:29
.=
((1 / 2) * ((cos (2 * (x + h))) - (cos (2 * x)))) / (((sin (x + h)) * (sin x)) ^2)
;
hence
(fD ((cot (#) cot),h)) . x = ((1 / 2) * ((cos (2 * (x + h))) - (cos (2 * x)))) / (((sin (x + h)) * (sin x)) ^2)
; verum