theorem :: DIFF_3:88

for h, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = (cot (#) cos) . x ) & x + (h / 2) in dom cot & x - (h / 2) in dom cot holds
(cD (f,h)) . x = (((1 / (sin (x + (h / 2)))) - (sin (x + (h / 2)))) - (1 / (sin (x - (h / 2))))) + (sin (x - (h / 2)))