let h, x be Real; :: thesis: ( 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 ) ; :: thesis: (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) )

proof

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

end;

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) ; :: thesis: verum