theorem :: DIFF_3:64

for h, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = 1 / (sin x) ) & sin (x + (h / 2)) <> 0 & sin (x - (h / 2)) <> 0 holds
(cD (f,h)) . x = - ((2 * ((sin (x - (h / 2))) - (sin (x + (h / 2))))) / ((cos (2 * x)) - (cos h)))