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