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