theorem :: FDIFF_10:30

for Z being open Subset of REAL st Z c= dom (exp_R (#) (tan - cot)) holds
( exp_R (#) (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R (#) (tan - cot)) `| Z) . x = ((exp_R . x) * ((tan . x) - (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ) )