theorem Th6: :: SINCOS10:6

( sec is_differentiable_on ].(PI / 2),PI.[ & ( for x being Real st x in ].(PI / 2),PI.[ holds
diff (sec,x) = (sin . x) / ((cos . x) ^2) ) )