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;
A3: 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:11;
hence sin . x <> 0 by FDIFF_8:2; :: thesis: verum

end;

A4: exp_R * cot is_differentiable_on Z by A1, FDIFF_8:17;
then A5: (- 1) (#) (exp_R * cot) is_differentiable_on Z by A2, FDIFF_1:20;
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 A6: x in Z ; :: thesis: ((- (exp_R * cot)) `| Z) . x = (exp_R . (cot . x)) / ((sin . x) ^2)
then A7: sin . x <> 0 by A3;
then A8: cot is_differentiable_in x by FDIFF_7:47;
A9: exp_R is_differentiable_in cot . x by SIN_COS:65;
A10: exp_R * cot is_differentiable_in x by A4, A6, FDIFF_1:9;
((- (exp_R * cot)) `| Z) . x = diff ((- (exp_R * cot)),x) by A5, A6, FDIFF_1:def 7
.= (- 1) * (diff ((exp_R * cot),x)) by A10, FDIFF_1:15
.= (- 1) * ((diff (exp_R,(cot . x))) * (diff (cot,x))) by A8, A9, FDIFF_2:13
.= (- 1) * ((diff (exp_R,(cot . x))) * (- (1 / ((sin . x) ^2)))) by A7, FDIFF_7:47
.= (- 1) * ((exp_R . (cot . x)) * (- (1 / ((sin . x) ^2)))) by SIN_COS:65
.= (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, A4, FDIFF_1:20; :: thesis: verum