theorem :: DIFF_4:16
for h, x being Real st x in dom sec & x - h in dom sec holds
(bD ((sec (#) sec),h)) . x = ((4 * (sin ((2 * x) - h))) * (sin h)) / (((cos ((2 * x) - h)) + (cos h)) ^2)