theorem :: DIFF_3:62

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 <> 0 & sin (x + h) <> 0 holds
(fD (f,h)) . x = - ((2 * ((sin x) - (sin (x + h)))) / ((cos ((2 * x) + h)) - (cos h)))