theorem Th1: :: FDIFF_9:1

for x being Real st cos . x <> 0 holds
( sec is_differentiable_in x & diff (sec,x) = (sin . x) / ((cos . x) ^2) )