theorem :: DIFF_3:82

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