let h, x be Real; :: thesis: ( x + (h / 2) in dom cot & x - (h / 2) in dom cot implies (cD ((cot (#) cot),h)) . x = ((1 / 2) * ((cos (h + (2 * x))) - (cos (h - (2 * x))))) / (((sin (x + (h / 2))) * (sin (x - (h / 2)))) ^2) )
set f = cot (#) cot;
assume A1: ( x + (h / 2) in dom cot & x - (h / 2) in dom cot ) ; :: thesis: (cD ((cot (#) cot),h)) . x = ((1 / 2) * ((cos (h + (2 * x))) - (cos (h - (2 * x))))) / (((sin (x + (h / 2))) * (sin (x - (h / 2)))) ^2)
A2: ( sin (x + (h / 2)) <> 0 & sin (x - (h / 2)) <> 0 ) by A1, FDIFF_8:2;
( x + (h / 2) in dom (cot (#) cot) & x - (h / 2) in dom (cot (#) cot) )

proof

( x + (h / 2) in (dom cot) /\ (dom cot) & x - (h / 2) in (dom cot) /\ (dom cot) ) by A1;
hence ( x + (h / 2) in dom (cot (#) cot) & x - (h / 2) in dom (cot (#) cot) ) by VALUED_1:def 4; :: thesis: verum

end;

then (cD ((cot (#) cot),h)) . x = ((cot (#) cot) . (x + (h / 2))) - ((cot (#) cot) . (x - (h / 2))) by DIFF_1:39
.= ((cot . (x + (h / 2))) * (cot . (x + (h / 2)))) - ((cot (#) cot) . (x - (h / 2))) by VALUED_1:5
.= ((cot . (x + (h / 2))) * (cot . (x + (h / 2)))) - ((cot . (x - (h / 2))) * (cot . (x - (h / 2)))) by VALUED_1:5
.= (((cos . (x + (h / 2))) * ((sin . (x + (h / 2))) ")) * (cot . (x + (h / 2)))) - ((cot . (x - (h / 2))) * (cot . (x - (h / 2)))) by A1, RFUNCT_1:def 1
.= (((cos . (x + (h / 2))) * ((sin . (x + (h / 2))) ")) * ((cos . (x + (h / 2))) * ((sin . (x + (h / 2))) "))) - ((cot . (x - (h / 2))) * (cot . (x - (h / 2)))) by A1, RFUNCT_1:def 1
.= (((cos . (x + (h / 2))) * ((sin . (x + (h / 2))) ")) * ((cos . (x + (h / 2))) * ((sin . (x + (h / 2))) "))) - (((cos . (x - (h / 2))) * ((sin . (x - (h / 2))) ")) * (cot . (x - (h / 2)))) by A1, RFUNCT_1:def 1
.= ((cot (x + (h / 2))) ^2) - ((cot (x - (h / 2))) ^2) by A1, RFUNCT_1:def 1
.= ((cot (x + (h / 2))) - (cot (x - (h / 2)))) * ((cot (x + (h / 2))) + (cot (x - (h / 2))))
.= (- ((sin ((x + (h / 2)) - (x - (h / 2)))) / ((sin (x + (h / 2))) * (sin (x - (h / 2)))))) * ((cot (x + (h / 2))) + (cot (x - (h / 2)))) by A2, SIN_COS4:24
.= (- ((sin h) / ((sin (x + (h / 2))) * (sin (x - (h / 2)))))) * ((sin ((x + (h / 2)) + (x - (h / 2)))) / ((sin (x + (h / 2))) * (sin (x - (h / 2))))) by A2, SIN_COS4:23
.= - (((sin h) / ((sin (x + (h / 2))) * (sin (x - (h / 2))))) * ((sin ((x + (h / 2)) + (x - (h / 2)))) / ((sin (x + (h / 2))) * (sin (x - (h / 2))))))
.= - (((sin h) * (sin (2 * x))) / (((sin (x + (h / 2))) * (sin (x - (h / 2)))) ^2)) by XCMPLX_1:76
.= - ((- ((1 / 2) * ((cos (h + (2 * x))) - (cos (h - (2 * x)))))) / (((sin (x + (h / 2))) * (sin (x - (h / 2)))) ^2)) by SIN_COS4:29
.= ((1 / 2) * ((cos (h + (2 * x))) - (cos (h - (2 * x))))) / (((sin (x + (h / 2))) * (sin (x - (h / 2)))) ^2) ;
hence (cD ((cot (#) cot),h)) . x = ((1 / 2) * ((cos (h + (2 * x))) - (cos (h - (2 * x))))) / (((sin (x + (h / 2))) * (sin (x - (h / 2)))) ^2) ; :: thesis: verum