theorem :: DIFF_3:79

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