theorem Th46: :: FDIFF_7:46

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