theorem :: DIFF_3:91

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