theorem :: DIFF_3:95

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