theorem :: DIFF_3:74

for h, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = 1 / ((cos x) ^2) ) & cos x <> 0 & cos (x + h) <> 0 holds
(fD (f,h)) . x = (((((- 16) * (sin (((2 * x) + h) / 2))) * (sin ((- h) / 2))) * (cos (((2 * x) + h) / 2))) * (cos ((- h) / 2))) / (((cos ((2 * x) + h)) + (cos h)) ^2)