theorem :: FDIFF_4:42

for Z being open Subset of REAL st Z c= dom (ln * cos) & ( for x being Real st x in Z holds
cos . x > 0 ) holds
( ln * cos is_differentiable_on Z & ( for x being Real st x in Z holds
((ln * cos) `| Z) . x = - (tan x) ) )