theorem :: DIFF_3:67

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