theorem Th5: :: SINCOS10:5

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