let Z be open Subset of REAL; :: thesis: ( Z c= dom (exp_R * cot) implies ( - (exp_R * cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (exp_R * cot)) `| Z) . x = (exp_R . (cot . x)) / ((sin . x) ^2) ) ) )
assume A1: Z c= dom (exp_R * cot) ; :: thesis: ( - (exp_R * cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (exp_R * cot)) `| Z) . x = (exp_R . (cot . x)) / ((sin . x) ^2) ) )
then A2: Z c= dom (- (exp_R * cot)) by VALUED_1:8;
B: for x being Real st x in Z holds
sin . x <> 0

proof

let x be Real; :: thesis: ( x in Z implies sin . x <> 0 )
assume x in Z ; :: thesis: sin . x <> 0
then x in dom (cos / sin) by A1, FUNCT_1:21;
hence sin . x <> 0 by FDIFF_8:2; :: thesis: verum

end;

A3: exp_R * cot is_differentiable_on Z by A1, FDIFF_8:17;
then A4: (- 1) (#) (exp_R * cot) is_differentiable_on Z by A2, FDIFF_1:28, A;
for x being Real st x in Z holds
((- (exp_R * cot)) `| Z) . x = (exp_R . (cot . x)) / ((sin . x) ^2)

proof

let x be Real; :: thesis: ( x in Z implies ((- (exp_R * cot)) `| Z) . x = (exp_R . (cot . x)) / ((sin . x) ^2) )
assume A5: x in Z ; :: thesis: ((- (exp_R * cot)) `| Z) . x = (exp_R . (cot . x)) / ((sin . x) ^2)
then A6: sin . x <> 0 by B;
then A7: cot is_differentiable_in x by FDIFF_7:47;
A8: exp_R is_differentiable_in cot . x by SIN_COS:70;
A9: exp_R * cot is_differentiable_in x by A3, A5, FDIFF_1:16;
((- (exp_R * cot)) `| Z) . x = diff ((- (exp_R * cot)),x) by A4, A5, FDIFF_1:def 8
.= (- 1) * (diff ((exp_R * cot),x)) by A9, FDIFF_1:23, A
.= (- 1) * ((diff (exp_R,(cot . x))) * (diff (cot,x))) by A7, A8, FDIFF_2:13
.= (- 1) * ((diff (exp_R,(cot . x))) * (- (1 / ((sin . x) ^2)))) by A6, FDIFF_7:47
.= (- 1) * ((exp_R . (cot . x)) * (- (1 / ((sin . x) ^2)))) by SIN_COS:70
.= (exp_R . (cot . x)) / ((sin . x) ^2) ;
hence ((- (exp_R * cot)) `| Z) . x = (exp_R . (cot . x)) / ((sin . x) ^2) ; :: thesis: verum

end;

hence ( - (exp_R * cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((- (exp_R * cot)) `| Z) . x = (exp_R . (cot . x)) / ((sin . x) ^2) ) ) by A2, A3, FDIFF_1:28, A; :: thesis: verum