theorem :: DIFF_3:96

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